Let x0 of type ο be given.

Assume H0: ∀ x1 . (∃ x2 : ι → ι . MetaCat_terminal_p EquivReln 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 EquivReln 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 EquivReln (pack_r 1 (λ x2 x3 . True)), ∀ x2 . EquivReln 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.

Apply unknownprop_46185b99972d7cc500b0fcea77da3881e5aca4376b72d7aefbcc4420b07dadec with 1, λ x2 x3 . True leaving 3 subgoals.

Let x2 of type ι be given.

Assume H2: x2 ∈ 1.

The subproof is completed by applying TrueI.

Let x2 of type ι be given.

Assume H2: x2 ∈ 1.

Let x3 of type ι be given.

Assume H3: x3 ∈ 1.

Assume H4: (λ x4 x5 . True) x2 x3.

The subproof is completed by applying TrueI.

Let x2 of type ι be given.

Assume H2: x2 ∈ 1.

Let x3 of type ι be given.

Assume H3: x3 ∈ 1.

Let x4 of type ι be given.

Assume H4: x4 ∈ 1.

Assume H5: (λ x5 x6 . True) x2 x3.

Assume H6: (λ x5 x6 . True) x3 x4.

The subproof is completed by applying TrueI.

Let x2 of type ι be given.

Assume H2: EquivReln x2.

Apply unknownprop_6402afcf89af96ded942e84b9859aeeef4ba7eaef1979737905398451311e541 with x2, λ 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)) leaving 2 subgoals.

The subproof is completed by applying H2.

Let x3 of type ι be given.

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

Assume H3: ∀ x5 . x5 ∈ x3 ⟶ x4 x5 x5.

Assume H4: ∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ x4 x5 x6 ⟶ x4 x6 x5.

Assume H5: ∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ x4 x5 x6 ⟶ x4 x6 x7 ⟶ x4 x5 x7.

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 ..., ... leaving 2 subgoals.

...

■

Proofgold Proof