α : Type u
β : Type v
γ : Type w
s1 s2 : Computation α
f : α → β
h1 : s1 ~ s2
⊢ LiftRel (fun x x_1 => x = x_1) (map f s1) (map f s2)
α : Type u
β : Type v
γ : Type w
s1 s2 : Computation α
f : α → β
h1 : s1 ~ s2
⊢ map f s1 ~ map f s2
rw [← lift_eq_iff_equiv]
no goals
α : Type u
β : Type v
γ : Type w
s1 s2 : Computation α
f : α → β
h1 : s1 ~ s2
⊢ LiftRel (fun x x_1 => x = x_1) (map f s1) (map f s2)
exact liftRel_map Eq _ ((lift_eq_iff_equiv _ _).2 h1) fun {a} b => congr_arg _