Let x0 of type ο be given.

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

Apply H0 with pack_r 1 (λ x1 x2 . True).

Let x1 of type ο be given.

Assume H1: ∀ x2 : ι → ι . MetaCat_terminal_p struct_r BinRelnHom struct_id struct_comp (pack_r 1 (λ x3 x4 . True)) x2 ⟶ x1.

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

Apply andI with struct_r (pack_r 1 (λ x2 x3 . True)), ∀ x2 . struct_r x2 ⟶ and (BinRelnHom x2 (pack_r 1 (λ x3 x4 . True)) (lam (ap x2 0) (λ x3 . 0))) (∀ x3 . BinRelnHom x2 (pack_r 1 (λ x4 x5 . True)) x3 ⟶ x3 = lam (ap x2 0) (λ x4 . 0)) leaving 2 subgoals.

The subproof is completed by applying pack_struct_r_I with 1, λ x2 x3 . True.

Let x2 of type ι be given.

Assume H2: struct_r x2.

Apply H2 with λ x3 . and (BinRelnHom x3 (pack_r 1 (λ x4 x5 . True)) (lam (ap x3 0) (λ x4 . 0))) (∀ x4 . BinRelnHom x3 (pack_r 1 (λ x5 x6 . True)) x4 ⟶ x4 = lam (ap x3 0) (λ x5 . 0)).

Let x3 of type ι be given.

Let x4 of type ι → ι → ο be given.

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

Apply pack_r_0_eq2 with x3, x4, λ x5 x6 . BinRelnHom (pack_r x3 x4) (pack_r 1 (λ x7 x8 . True)) (lam x5 (λ x7 . 0)).

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

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

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

Let x5 of type ι be given.

Assume H3: x5 ∈ x3.

The subproof is completed by applying In_0_1.

Let x5 of type ι be given.

Assume H3: x5 ∈ x3.

Let x6 of type ι be given.

Assume H4: x6 ∈ x3.

Assume H5: x4 x5 x6.

The subproof is completed by applying TrueI.

Let x5 of type ι be given.

Apply unknownprop_4e486761c3790f4990f398ce8c16ea7ac5915924a294f8e5b06e45030e68e983 with x3, 1, x4, λ x6 x7 . True, x5, λ x6 x7 : ο . x7 ⟶ x5 = lam (ap (pack_r x3 x4) 0) (λ x8 . 0).

Assume H3: and (x5 ∈ setexp 1 x3) (∀ x6 . ... ⟶ ∀ x7 . ... ⟶ x4 x6 ... ⟶ (λ x8 x9 . True) (ap x5 x6) (ap x5 x7)).

...

■

Proofgold Proof