α : Type u
β : Type v
γ : Type w
R : α → β → Prop
a : α
b : β
s : WSeq α
t : WSeq β
⊢ Computation.LiftRel (LiftRelO R (LiftRel R)) (destruct (cons a s)) (destruct (cons b t)) ↔ R a b ∧ LiftRel R s t
α : Type u
β : Type v
γ : Type w
R : α → β → Prop
a : α
b : β
s : WSeq α
t : WSeq β
⊢ LiftRel R (cons a s) (cons b t) ↔ R a b ∧ LiftRel R s t
rw [liftRel_destruct_iff]
no goals
α : Type u
β : Type v
γ : Type w
R : α → β → Prop
a : α
b : β
s : WSeq α
t : WSeq β
⊢ Computation.LiftRel (LiftRelO R (LiftRel R)) (destruct (cons a s)) (destruct (cons b t)) ↔ R a b ∧ LiftRel R s t
simp [-liftRel_pure_left, -liftRel_pure_right]