α : Type u
β : Type v
γ : Type w
R : α → β → Prop
ca : Computation α
cb : Computation β
⊢ LiftRel (swap R) (think cb) ca ↔ LiftRel (swap R) cb ca
α : Type u
β : Type v
γ : Type w
R : α → β → Prop
ca : Computation α
cb : Computation β
⊢ LiftRel R ca (think cb) ↔ LiftRel R ca cb
rw [← LiftRel.swap R, ← LiftRel.swap R]
no goals
α : Type u
β : Type v
γ : Type w
R : α → β → Prop
ca : Computation α
cb : Computation β
⊢ LiftRel (swap R) (think cb) ca ↔ LiftRel (swap R) cb ca
apply liftRel_think_left