no goals
α : Type u
β : Type v
γ : Type w
R : α → β → Prop
C : Computation α → Computation β → Prop
b : β
ca : Computation α
⊢ LiftRelAux R C (destruct ca) (Sum.inl b) ↔ ∃ a, a ∈ ca ∧ R a b
rw [← LiftRelAux.swap, LiftRelAux.ret_left]