Let x0 of type ι → ο be given.

Assume H0: x0 1.

Assume H1: x0 2.

Let x1 of type ο be given.

Assume H2: ∀ x2 . (∃ x3 : ι → ι . ∃ x4 x5 . ∃ x6 : ι → ι → ι → ι . ∃ x7 : ι → ι → ι → ι → ι → ι → ι . MetaCat_subobject_classifier_p x0 HomSet (λ x8 . lam_id x8) (λ x8 x9 x10 x11 x12 . lam_comp x8 x11 x12) x2 x3 x4 x5 x6 x7) ⟶ x1.

Apply H2 with 1.

Let x2 of type ο be given.

Assume H3: ∀ x3 : ι → ι . (∃ x4 x5 . ∃ x6 : ι → ι → ι → ι . ∃ x7 : ι → ι → ι → ι → ι → ι → ι . MetaCat_subobject_classifier_p x0 HomSet (λ x8 . lam_id x8) (λ x8 x9 x10 x11 x12 . lam_comp x8 x11 x12) 1 x3 x4 x5 x6 x7) ⟶ x2.

Apply H3 with λ x3 . lam x3 (λ x4 . 0).

Let x3 of type ο be given.

Assume H4: ∀ x4 . (∃ x5 . ∃ x6 : ι → ι → ι → ι . ∃ x7 : ι → ι → ι → ι → ι → ι → ι . MetaCat_subobject_classifier_p x0 HomSet (λ x8 . lam_id x8) (λ x8 x9 x10 x11 x12 . lam_comp x8 x11 x12) 1 (λ x8 . lam x8 (λ x9 . 0)) x4 x5 x6 x7) ⟶ x3.

Apply H4 with 2.

Let x4 of type ο be given.

Assume H5: ∀ x5 . (∃ x6 : ι → ι → ι → ι . ∃ x7 : ι → ι → ι → ι → ι → ι → ι . MetaCat_subobject_classifier_p x0 HomSet (λ x8 . lam_id x8) (λ x8 x9 x10 x11 x12 . lam_comp x8 x11 x12) 1 (λ x8 . lam x8 (λ x9 . 0)) 2 x5 x6 x7) ⟶ x4.

Apply H5 with lam 1 (λ x5 . 1).

Let x5 of type ο be given.

Assume H6: ∀ x6 : ι → ι → ι → ι . (∃ x7 : ι → ι → ι → ι → ι → ι → ι . MetaCat_subobject_classifier_p x0 HomSet (λ x8 . lam_id x8) (λ x8 x9 x10 x11 x12 . lam_comp x8 x11 x12) 1 (λ x8 . lam x8 (λ x9 . 0)) 2 (lam 1 (λ x8 . 1)) x6 x7) ⟶ x5.

Apply H6 with λ x6 x7 x8 . lam x7 (λ x9 . If_i (∃ x10 . and (x10 ∈ x6) (ap x8 x10 = x9)) 1 0).

Let x6 of type ο be given.

Assume H7: ∀ x7 : ι → ι → ι → ι → ι → ι → ι . MetaCat_subobject_classifier_p x0 HomSet (λ x8 . lam_id x8) (λ x8 x9 x10 x11 x12 . lam_comp x8 x11 x12) 1 (λ x8 . lam x8 (λ x9 . 0)) 2 (lam 1 (λ x8 . 1)) (λ x8 x9 x10 . lam x9 (λ x11 . If_i (∃ x12 . and (x12 ∈ x8) (ap x10 x12 = x11)) 1 0)) x7 ⟶ x6.

Apply H7 with λ x7 x8 x9 x10 x11 x12 . lam x10 (λ x13 . inv x7 (λ x14 . ap x9 x14) (ap x12 x13)).

Apply unknownprop_37ccacf65044aaad4e34d83b49209a18a03855b2543d0d1b3289fe130b0ae296 with x0 leaving 2 subgoals.

The subproof is completed by applying H0.

The subproof is completed by applying H1.

■

Proofgold Proof