no goals
α : Type u
β : Type v
γ : Type w
R : α → β → Prop
C : Computation α → Computation β → Prop
a : α ⊕ Computation α
b : β ⊕ Computation β
⊢ LiftRelAux (Function.swap R) (Function.swap C) b a = LiftRelAux R C a b
cases' a with a ca <;> cases' b with b cb <;> simp only [LiftRelAux]