Let x0 of type ο be given.

Assume H0: ∀ x1 : ι → ι → ι . (∃ x2 x3 : ι → ι → ι . ∃ x4 : ι → ι → ι → ι → ι → ι . MetaCat_coproduct_constr_p IrreflexiveTransitiveReln BinRelnHom struct_id struct_comp x1 x2 x3 x4) ⟶ x0.

Apply H0 with 3fa3a...

Let x1 of type ο be given.

Assume H1: ∀ x2 : ι → ι → ι . (∃ x3 : ι → ι → ι . ∃ x4 : ι → ι → ι → ι → ι → ι . MetaCat_coproduct_constr_p IrreflexiveTransitiveReln BinRelnHom struct_id struct_comp 3fa3a.. x2 x3 x4) ⟶ x1.

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

Let x2 of type ο be given.

Assume H2: ∀ x3 : ι → ι → ι . (∃ x4 : ι → ι → ι → ι → ι → ι . MetaCat_coproduct_constr_p IrreflexiveTransitiveReln BinRelnHom struct_id struct_comp 3fa3a.. (λ x5 x6 . lam (ap x5 0) (λ x7 . Inj0 x7)) x3 x4) ⟶ x2.

Apply H2 with λ x3 x4 . lam (ap x4 0) (λ x5 . Inj1 x5).

Let x3 of type ο be given.

Assume H3: ∀ x4 : ι → ι → ι → ι → ι → ι . MetaCat_coproduct_constr_p IrreflexiveTransitiveReln BinRelnHom struct_id struct_comp 3fa3a.. (λ x5 x6 . lam (ap x5 0) (λ x7 . Inj0 x7)) (λ x5 x6 . lam (ap x6 0) (λ x7 . Inj1 x7)) x4 ⟶ x3.

Apply H3 with λ x4 x5 x6 x7 x8 . lam (setsum (ap x4 0) (ap x5 0)) (λ x9 . combine_funcs (ap x4 0) (ap x5 0) (λ x10 . ap x7 x10) (λ x10 . ap x8 x10) x9).

Apply unknownprop_8014f2189a8e9a90722a83ab5f5b4d52ecd6d5c686aac8aa2eb5343a4f9f7780 with IrreflexiveTransitiveReln leaving 2 subgoals.

Let x4 of type ι be given.

Assume H4: IrreflexiveTransitiveReln x4.

Apply H4 with struct_r x4.

Assume H5: struct_r x4.

Assume H6: unpack_r_o x4 (λ x5 . λ x6 : ι → ι → ο . and (∀ x7 . x7 ∈ x5 ⟶ not (x6 x7 x7)) (∀ x7 . x7 ∈ x5 ⟶ ∀ x8 . x8 ∈ x5 ⟶ ∀ x9 . x9 ∈ x5 ⟶ x6 x7 x8 ⟶ x6 x8 x9 ⟶ x6 x7 x9)).

The subproof is completed by applying H5.

Let x4 of type ι be given.

Let x5 of type ι be given.

Assume H4: IrreflexiveTransitiveReln x4.

Assume H5: IrreflexiveTransitiveReln x5.

Apply unknownprop_2d7c7a9916fa2967cfb4d546f4e37c43b64368ed4a60618379328e066e9b7e0e with x4, λ x6 . IrreflexiveTransitiveReln (3fa3a.. x6 x5) leaving 2 subgoals.

The subproof is completed by applying H4.

Let x6 of type ι be given.

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

Assume H6: ∀ x8 . x8 ∈ x6 ⟶ not (x7 x8 x8).

Assume H7: ∀ x8 . x8 ∈ x6 ⟶ ∀ x9 . x9 ∈ x6 ⟶ ∀ x10 . x10 ∈ x6 ⟶ x7 x8 x9 ⟶ x7 x9 x10 ⟶ x7 x8 x10.

Apply unknownprop_2d7c7a9916fa2967cfb4d546f4e37c43b64368ed4a60618379328e066e9b7e0e with x5, λ x8 . IrreflexiveTransitiveReln (3fa3a.. (pack_r x6 x7) x8) leaving 2 subgoals.

The subproof is completed by applying H5.

Let x8 of type ι be given.

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

Assume H8: ∀ x10 . x10 ∈ x8 ⟶ not (x9 x10 x10).

Assume H9: ∀ x10 . x10 ∈ x8 ⟶ ∀ x11 . x11 ∈ x8 ⟶ ∀ x12 . x12 ∈ x8 ⟶ x9 x10 x11 ⟶ x9 x11 x12 ⟶ x9 x10 x12.

Apply unknownprop_2b21d9fc231c558646c467d14a820e3bc5f0cce785ca7db2a0cb0c92dadc07f5 with x6, x7, x8, x9, λ x10 x11 . IrreflexiveTransitiveReln x11.

Apply unknownprop_dbb6377af3127d2bf8cd888143d856b4a86f0ec975822a440e0313d91ee07474 with setsum x6 x8, λ x10 x11 . or (and (and ... ...) ...) ... leaving 2 subgoals.

...

■

Proofgold Proof