left
case a.refl.Free.a
C : _root_.Container
R : Type u₁
x : Free C R
node : C.A
k : Container.B C node → Free C R
y : Container.B C node
⊢ ((fun x y => x = y) ⊔ pequiv Eq fun x y => x = y) (k y) (k y)
case a.refl.Free.a.h
C : _root_.Container
R : Type u₁
x : Free C R
node : C.A
k : Container.B C node → Free C R
y : Container.B C node
⊢ (fun x y => x = y) (k y) (k y)