Assume H0: ∃ x0 : ι → ι . ∃ x1 : ι → ι → ι → ι . ∃ x2 x3 : ι → ι . MetaAdjunction_strict (λ x4 . True) HomSet lam_id (λ x4 x5 x6 . lam_comp x4) PtdPred UnaryPredHom struct_id struct_comp x0 x1 (λ x4 . ap x4 0) (λ x4 x5 x6 . x6) x2 x3.

Apply H0 with False.

Let x0 of type ι → ι be given.

Assume H1: (λ x1 : ι → ι . ∃ x2 : ι → ι → ι → ι . ∃ x3 x4 : ι → ι . MetaAdjunction_strict (λ x5 . True) HomSet lam_id (λ x5 x6 x7 . lam_comp x5) PtdPred UnaryPredHom struct_id struct_comp x1 x2 (λ x5 . ap x5 0) (λ x5 x6 x7 . x7) x3 x4) x0.

Apply H1 with False.

Let x1 of type ι → ι → ι → ι be given.

Assume H2: (λ x2 : ι → ι → ι → ι . ∃ x3 x4 : ι → ι . MetaAdjunction_strict (λ x5 . True) HomSet lam_id (λ x5 x6 x7 . lam_comp x5) PtdPred UnaryPredHom struct_id struct_comp x0 x2 (λ x5 . ap x5 0) (λ x5 x6 x7 . x7) x3 x4) x1.

Apply H2 with False.

Let x2 of type ι → ι be given.

Assume H3: (λ x3 : ι → ι . ∃ x4 : ι → ι . MetaAdjunction_strict (λ x5 . True) HomSet lam_id (λ x5 x6 x7 . lam_comp x5) PtdPred UnaryPredHom struct_id struct_comp x0 x1 (λ x5 . ap x5 0) (λ x5 x6 x7 . x7) x3 x4) x2.

Apply H3 with False.

Let x3 of type ι → ι be given.

Assume H4: MetaAdjunction_strict (λ x4 . True) HomSet (λ x4 . lam_id x4) (λ x4 x5 x6 x7 x8 . lam_comp x4 x7 x8) PtdPred UnaryPredHom struct_id struct_comp x0 x1 (λ x4 . ap x4 0) (λ x4 x5 x6 . x6) x2 x3.

Apply unknownprop_9a5dd92d37ccfa65696c11e832d98097811bf4001ca7eb00f4f9586fc6e6bb6b with λ x4 . True, HomSet, lam_id, λ x4 x5 x6 x7 x8 . lam_comp x4 x7 x8, PtdPred, UnaryPredHom, struct_id, struct_comp, x0, x1, λ x4 . ap x4 0, λ x4 x5 x6 . x6, x2, x3, False leaving 2 subgoals.

The subproof is completed by applying H4.

Assume H5: MetaFunctor_strict (λ x4 . True) HomSet lam_id (λ x4 x5 x6 . lam_comp x4) PtdPred UnaryPredHom struct_id struct_comp x0 x1.

Assume H6: MetaFunctor PtdPred UnaryPredHom struct_id struct_comp (λ x4 . True) HomSet lam_id (λ x4 x5 x6 . lam_comp x4) (λ x4 . ap x4 0) (λ x4 x5 x6 . x6).

Assume H7: MetaNatTrans (λ x4 . True) HomSet lam_id (λ x4 x5 x6 . lam_comp x4) (λ x4 . True) HomSet lam_id (λ x4 x5 x6 . lam_comp x4) (λ x4 . x4) (λ x4 x5 x6 . x6) (λ x4 . ap (x0 x4) 0) x1 x2.

Assume H8: MetaNatTrans PtdPred UnaryPredHom struct_id struct_comp PtdPred UnaryPredHom struct_id struct_comp (λ x4 . x0 (ap x4 0)) (λ x4 x5 . x1 (ap x4 0) (ap x5 0)) (λ x4 . x4) (λ x4 x5 x6 . x6) x3.

Assume H9: MetaAdjunction (λ x4 . True) HomSet lam_id (λ x4 x5 x6 . lam_comp x4) PtdPred UnaryPredHom ... ... ... ... ... ... ... ....

...

■

Proofgold Proof