Let x0 of type ι be given.

Assume H0: dac20.. x0.

Apply H0 with d7e73.. x0.

Assume H1: 3f0d0.. x0.

Claim L2: c3510.. x0 (λ x1 . λ x2 x3 : ι → ι → ι . λ x4 x5 . explicit_CRing_with_id x1 x4 x5 x2 x3) ⟶ c3510.. x0 (λ x1 . λ x2 x3 : ι → ι → ι . λ x4 x5 . explicit_Ring_with_id x1 x4 x5 x2 x3)

Apply H1 with λ x1 . c3510.. x1 (λ x2 . λ x3 x4 : ι → ι → ι . λ x5 x6 . explicit_CRing_with_id x2 x5 x6 x3 x4) ⟶ c3510.. x1 (λ x2 . λ x3 x4 : ι → ι → ι . λ x5 x6 . explicit_Ring_with_id x2 x5 x6 x3 x4).

Let x1 of type ι be given.

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

Assume H2: ∀ x3 . prim1 x3 x1 ⟶ ∀ x4 . prim1 x4 x1 ⟶ prim1 (x2 x3 x4) x1.

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

Assume H3: ∀ x4 . prim1 x4 x1 ⟶ ∀ x5 . prim1 x5 x1 ⟶ prim1 (x3 x4 x5) x1.

Let x4 of type ι be given.

Assume H4: prim1 x4 x1.

Let x5 of type ι be given.

Assume H5: prim1 x5 x1.

Apply unknownprop_012ca8caa2f09e68def42ddb439cd4e9c3f98b6e2edd38830763ab994ab639cc with x1, x2, x3, x4, x5, λ x6 x7 : ο . x7 ⟶ c3510.. (c77b5.. x1 x2 x3 x4 x5) (λ x8 . λ x9 x10 : ι → ι → ι . λ x11 x12 . explicit_Ring_with_id x8 x11 x12 x9 x10).

Apply unknownprop_f2757170e44f67f7fbfc05bcf8ee9518d90964960839997db64166d5bcc81904 with x1, x2, x3, x4, x5, λ x6 x7 : ο . explicit_CRing_with_id x1 x4 x5 x2 x3 ⟶ x7.

The subproof is completed by applying explicit_CRing_with_id_Ring_with_id with x1, x4, x5, x2, x3.

Assume H3: c3510.. x0 (λ x1 . λ x2 x3 : ι → ι → ι . λ x4 x5 . explicit_CRing_with_id x1 x4 x5 x2 x3).

Apply andI with 3f0d0.. x0, c3510.. x0 (λ x1 . λ x2 x3 : ι → ι → ι . λ x4 x5 . explicit_Ring_with_id x1 x4 x5 x2 x3) leaving 2 subgoals.

The subproof is completed by applying H1.

Apply L2.

The subproof is completed by applying H3.

■

Proofgold Proof