α : Type u
β : Type v
γ : Type w
R : α → β → Prop
s1 : WSeq α
s2 : WSeq β
h✝ : LiftRel R s1 s2
s : WSeq β
t : WSeq α
h : LiftRel R t s
⊢ Computation.LiftRel (LiftRelO (swap R) (swap (LiftRel R))) (destruct s) (destruct t)
α : Type u
β : Type v
γ : Type w
R : α → β → Prop
s1 : WSeq α
s2 : WSeq β
h : LiftRel R s1 s2
⊢ LiftRel (swap R) s2 s1
refine' ⟨swap (LiftRel R), h, fun {s t} (h : LiftRel R t s) => _⟩
α : Type u
β : Type v
γ : Type w
R : α → β → Prop
s1 : WSeq α
s2 : WSeq β
h✝ : LiftRel R s1 s2
s : WSeq β
t : WSeq α
h : LiftRel R t s
⊢ Computation.LiftRel (LiftRelO R (LiftRel R)) (destruct t) (destruct s)
α : Type u
β : Type v
γ : Type w
R : α → β → Prop
s1 : WSeq α
s2 : WSeq β
h✝ : LiftRel R s1 s2
s : WSeq β
t : WSeq α
h : LiftRel R t s
⊢ Computation.LiftRel (LiftRelO (swap R) (swap (LiftRel R))) (destruct s) (destruct t)
rw [← LiftRelO.swap, Computation.LiftRel.swap]
no goals
α : Type u
β : Type v
γ : Type w
R : α → β → Prop
s1 : WSeq α
s2 : WSeq β
h✝ : LiftRel R s1 s2
s : WSeq β
t : WSeq α
h : LiftRel R t s
⊢ Computation.LiftRel (LiftRelO R (LiftRel R)) (destruct t) (destruct s)
apply liftRel_destruct h