exists (A.Free node)
case h₀.Free
C : _root_.Container
R : Type u₁
node : C.A
k₁ k₂ : Container.B C node → Free C R
h : ∀ (x : Container.B C node), (⊥ ⊔ ↑(pgfp (equivF' Eq)) ⊥) (k₁ x) (k₂ x)
⊢ ∃ node_1 k₁_1 k₂_1,
    M.destruct (construct (Functor.Free node k₁)) = { fst := node_1, snd := k₁_1 } ∧
      M.destruct (construct (Functor.Free node k₂)) = { fst := node_1, snd := k₂_1 } ∧
        ∀ (i : Container.B (Container C R) node_1), eq (k₁_1 i) (k₂_1 i)
case h₀.Free
C : _root_.Container
R : Type u₁
node : C.A
k₁ k₂ : Container.B C node → Free C R
h : ∀ (x : Container.B C node), (⊥ ⊔ ↑(pgfp (equivF' Eq)) ⊥) (k₁ x) (k₂ x)
⊢ ∃ k₁_1 k₂_1,
    M.destruct (construct (Functor.Free node k₁)) = { fst := A.Free node, snd := k₁_1 } ∧
      M.destruct (construct (Functor.Free node k₂)) = { fst := A.Free node, snd := k₂_1 } ∧
        ∀ (i : Container.B (Container C R) (A.Free node)), eq (k₁_1 i) (k₂_1 i)