Let x0 of type ο be given.

Assume H0: ∀ x1 . (∃ x2 : ι → ι . MetaCat_terminal_p PtdPred UnaryPredHom struct_id struct_comp x1 x2) ⟶ x0.

Apply H0 with pack_p 1 (λ x1 . True).

Let x1 of type ο be given.

Assume H1: ∀ x2 : ι → ι . MetaCat_terminal_p PtdPred UnaryPredHom struct_id struct_comp (pack_p 1 (λ x3 . True)) x2 ⟶ x1.

Apply H1 with λ x2 . lam (ap x2 0) (λ x3 . 0).

Apply andI with PtdPred (pack_p 1 (λ x2 . True)), ∀ x2 . PtdPred x2 ⟶ and (UnaryPredHom x2 (pack_p 1 (λ x3 . True)) (lam (ap x2 0) (λ x3 . 0))) (∀ x3 . UnaryPredHom x2 (pack_p 1 (λ x4 . True)) x3 ⟶ x3 = lam (ap x2 0) (λ x4 . 0)) leaving 2 subgoals.

Apply unknownprop_2576d2815b46016e5e13a9989b4e9789629d83c56ed1c92a4cda0de077a20752 with 1, λ x2 . True.

Let x2 of type ο be given.

Assume H2: ∀ x3 . and (x3 ∈ 1) ((λ x4 . True) x3) ⟶ x2.

Apply H2 with 0.

Apply andI with 0 ∈ 1, (λ x3 . True) 0 leaving 2 subgoals.

The subproof is completed by applying In_0_1.

The subproof is completed by applying TrueI.

Let x2 of type ι be given.

Assume H2: PtdPred x2.

Apply unknownprop_c86200a2eefb0ff844f50b29d5cbeaa2ee14856a2db63542bcbf63218f0d0f1e with x2, λ x3 . and (UnaryPredHom x3 (pack_p 1 (λ x4 . True)) (lam (ap x3 0) (λ x4 . 0))) (∀ x4 . UnaryPredHom x3 (pack_p 1 (λ x5 . True)) x4 ⟶ x4 = lam (ap x3 0) (λ x5 . 0)) leaving 2 subgoals.

The subproof is completed by applying H2.

Let x3 of type ι be given.

Let x4 of type ι → ο be given.

Let x5 of type ι be given.

Assume H3: x5 ∈ x3.

Assume H4: x4 x5.

Apply andI with UnaryPredHom (pack_p x3 x4) (pack_p 1 (λ x6 . True)) (lam (ap (pack_p x3 x4) 0) (λ x6 . 0)), ∀ x6 . UnaryPredHom (pack_p x3 x4) (pack_p 1 (λ x7 . True)) x6 ⟶ x6 = lam (ap (pack_p x3 x4) 0) (λ x7 . 0) leaving 2 subgoals.

Apply pack_p_0_eq2 with x3, x4, λ x6 x7 . UnaryPredHom (pack_p x3 x4) (pack_p 1 (λ x8 . True)) (lam x6 (λ x8 . 0)).

Apply unknownprop_63c01b8f599732ba7bc3b48c28c0f10755230e5cc9f0717c7895602d2eaf01d3 with x3, 1, x4, λ x6 . True, lam x3 (λ x6 . 0), λ x6 x7 : ο . x7.

Apply andI with lam x3 (λ x6 . 0) ∈ setexp 1 x3, ∀ x6 . x6 ∈ x3 ⟶ x4 x6 ⟶ (λ x7 . True) (ap (lam x3 (λ x7 . 0)) x6) leaving 2 subgoals.

Apply lam_Pi with x3, λ x6 . 1, λ x6 . 0.

Let x6 of type ι be given.

Assume H5: x6 ∈ x3.

The subproof is completed by applying In_0_1.

Let x6 of type ι be given.

Assume H5: x6 ∈ x3.

Assume H6: x4 x6.

The subproof is completed by applying TrueI.

Let x6 of type ι be given.

Apply unknownprop_63c01b8f599732ba7bc3b48c28c0f10755230e5cc9f0717c7895602d2eaf01d3 with x3, 1, x4, λ x7 . True, x6, λ x7 x8 : ο . x8 ⟶ x6 = lam (ap (pack_p x3 x4) 0) (λ x9 . 0).

Assume H5: and (x6 ∈ setexp 1 x3) (∀ x7 . ... ⟶ x4 ... ⟶ True).

...

■

Proofgold Proof