α : Type u
β : Type v
γ : Type w
R : α → β → Prop
s : WSeq α
t : WSeq β
⊢ Computation.LiftRel (LiftRelO R (LiftRel R)) (destruct (think s)) (destruct t) ↔
    Computation.LiftRel (LiftRelO R (LiftRel R)) (destruct s) (destruct t)
α : Type u
β : Type v
γ : Type w
R : α → β → Prop
s : WSeq α
t : WSeq β
⊢ LiftRel R (think s) t ↔ LiftRel R s t
rw [liftRel_destruct_iff, liftRel_destruct_iff]
no goals
α : Type u
β : Type v
γ : Type w
R : α → β → Prop
s : WSeq α
t : WSeq β
⊢ Computation.LiftRel (LiftRelO R (LiftRel R)) (destruct (think s)) (destruct t) ↔
    Computation.LiftRel (LiftRelO R (LiftRel R)) (destruct s) (destruct t)
simp