Assume H0: ∃ x0 . ∃ x1 : ι → ι . ∃ x2 x3 x4 . ∃ x5 : ι → ι → ι → ι . MetaCat_nno_p IrreflexiveSymmetricReln BinRelnHom struct_id struct_comp x0 x1 x2 x3 x4 x5.

Apply H0 with False.

Let x0 of type ι be given.

Assume H1: (λ x1 . ∃ x2 : ι → ι . ∃ x3 x4 x5 . ∃ x6 : ι → ι → ι → ι . MetaCat_nno_p IrreflexiveSymmetricReln BinRelnHom struct_id struct_comp x1 x2 x3 x4 x5 x6) x0.

Apply H1 with False.

Let x1 of type ι → ι be given.

Assume H2: (λ x2 : ι → ι . ∃ x3 x4 x5 . ∃ x6 : ι → ι → ι → ι . MetaCat_nno_p IrreflexiveSymmetricReln BinRelnHom struct_id struct_comp x0 x2 x3 x4 x5 x6) x1.

Apply H2 with False.

Let x2 of type ι be given.

Assume H3: (λ x3 . ∃ x4 x5 . ∃ x6 : ι → ι → ι → ι . MetaCat_nno_p IrreflexiveSymmetricReln BinRelnHom struct_id struct_comp x0 x1 x3 x4 x5 x6) x2.

Apply H3 with False.

Let x3 of type ι be given.

Assume H4: (λ x4 . ∃ x5 . ∃ x6 : ι → ι → ι → ι . MetaCat_nno_p IrreflexiveSymmetricReln BinRelnHom struct_id struct_comp x0 x1 x2 x4 x5 x6) x3.

Apply H4 with False.

Let x4 of type ι be given.

Assume H5: (λ x5 . ∃ x6 : ι → ι → ι → ι . MetaCat_nno_p IrreflexiveSymmetricReln BinRelnHom struct_id struct_comp x0 x1 x2 x3 x5 x6) x4.

Apply H5 with False.

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

Assume H6: MetaCat_nno_p IrreflexiveSymmetricReln BinRelnHom struct_id struct_comp x0 x1 x2 x3 x4 x5.

Apply H6 with False.

Assume H7: and (and (and (MetaCat_terminal_p IrreflexiveSymmetricReln BinRelnHom struct_id struct_comp x0 x1) (IrreflexiveSymmetricReln x2)) (BinRelnHom x0 x2 x3)) (BinRelnHom x2 x2 x4).

Apply H7 with (∀ x6 x7 x8 . IrreflexiveSymmetricReln x6 ⟶ BinRelnHom x0 x6 x7 ⟶ BinRelnHom x6 x6 x8 ⟶ and (and (and (BinRelnHom x2 x6 (x5 x6 x7 x8)) (struct_comp x0 x2 x6 (x5 x6 x7 x8) x3 = x7)) (struct_comp x2 x2 x6 (x5 x6 x7 x8) x4 = struct_comp x2 x6 x6 x8 (x5 x6 x7 x8))) (∀ x9 . BinRelnHom x2 x6 x9 ⟶ struct_comp x0 x2 x6 x9 x3 = x7 ⟶ struct_comp x2 x2 x6 x9 x4 = struct_comp x2 x6 x6 x8 x9 ⟶ x9 = x5 x6 x7 x8)) ⟶ False.

Assume H8: and (and (MetaCat_terminal_p IrreflexiveSymmetricReln BinRelnHom struct_id struct_comp x0 x1) (IrreflexiveSymmetricReln x2)) (BinRelnHom x0 x2 x3).

Apply H8 with ... ⟶ (∀ x6 x7 x8 . ... ⟶ ... ⟶ ... ⟶ and (and (and (BinRelnHom x2 x6 (x5 x6 x7 x8)) (struct_comp x0 x2 x6 (x5 x6 ... ...) ... = ...)) ...) ...) ⟶ False.

...

■

Proofgold Proof