Why Quotient Lifted function is compatible?

Stream: general

[Erika Su]

How do i know the function obtained with Quotient.lift is compatible with Quotient.mk? As in the following.

section liftedquotient
variable (s1 s2 s3 : Setoid α )
variable (f : α -> β)
theorem respect : ∀ x y : α , s1.r x y -> f x = f y := .....

theorem lifted_compatible : (x : α) -> (Quotient.mk s1 x).liftOn f (respect _ _ )  = f x := sorry -- how to prove?

end liftedquotient

Also, do lean have a typeclass for Respect Fn R, meaning that Fn respect R?

[Adam Topaz]

It should be true by rfl