cases h
case a
C : _root_.Container
R : Type u₁
x y : Free C R
h : x = y
⊢ equivF Eq ((fun x y => x = y) ⊔ pequiv Eq fun x y => x = y) x y
case a.refl
C : _root_.Container
R : Type u₁
x : Free C R
⊢ equivF Eq ((fun x y => x = y) ⊔ pequiv Eq fun x y => x = y) x x