α : Type u
β : Type v
γ : Type w
R : α → β → Prop
⊢ Computation.LiftRel (LiftRelO R (LiftRel R)) (destruct nil) (destruct nil)
α : Type u
β : Type v
γ : Type w
R : α → β → Prop
⊢ LiftRel R nil nil
rw [liftRel_destruct_iff]
no goals
α : Type u
β : Type v
γ : Type w
R : α → β → Prop
⊢ Computation.LiftRel (LiftRelO R (LiftRel R)) (destruct nil) (destruct nil)
simp [-liftRel_pure_left, -liftRel_pure_right]