Let x0 of type ο be given.

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

Apply H0 with BinReln_product.

Let x1 of type ο be given.

Assume H1: ∀ x2 : ι → ι → ι . (∃ x3 : ι → ι → ι . ∃ x4 : ι → ι → ι → ι → ι → ι . MetaCat_product_constr_p IrreflexiveTransitiveReln BinRelnHom struct_id struct_comp BinReln_product x2 x3 x4) ⟶ x1.

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

Let x2 of type ο be given.

Assume H2: ∀ x3 : ι → ι → ι . (∃ x4 : ι → ι → ι → ι → ι → ι . MetaCat_product_constr_p IrreflexiveTransitiveReln BinRelnHom struct_id struct_comp BinReln_product (λ x5 x6 . lam (setprod (ap x5 0) (ap x6 0)) (λ x7 . ap x7 0)) x3 x4) ⟶ x2.

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

Let x3 of type ο be given.

Assume H3: ∀ x4 : ι → ι → ι → ι → ι → ι . MetaCat_product_constr_p IrreflexiveTransitiveReln BinRelnHom struct_id struct_comp BinReln_product (λ x5 x6 . lam (setprod (ap x5 0) (ap x6 0)) (λ x7 . ap x7 0)) (λ x5 x6 . lam (setprod (ap x5 0) (ap x6 0)) (λ x7 . ap x7 1)) x4 ⟶ x3.

Apply H3 with λ x4 x5 x6 x7 x8 . lam (ap x6 0) (λ x9 . lam 2 (λ x10 . If_i (x10 = 0) (ap x7 x9) (ap x8 x9))).

Apply unknownprop_5f5149dc445b1bf6ca4a7f60e27b87771b4704fa8e9610ac4ab806ac27b93c0b with IrreflexiveTransitiveReln leaving 2 subgoals.

The subproof is completed by applying unknownprop_d843c34578125329414df28865a610fdc4b3dedf56de3dd9e99c774f88282c4d.

The subproof is completed by applying unknownprop_adf9af6df0ab9ce6906c8af96b0e8b5f458fb0d3ac8ad3a40c928c13a16dac6a.

■

Proofgold Proof