Let x0 of type ι be given.

Assume H0: 38cca.. x0.

Apply H0 with dac20.. x0.

Assume H1: 3f0d0.. x0.

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

Apply H1 with λ x1 . c3510.. x1 (λ x2 . λ x3 x4 : ι → ι → ι . λ x5 x6 . explicit_Field x2 x5 x6 x3 x4) ⟶ c3510.. x1 (λ x2 . λ x3 x4 : ι → ι → ι . λ x5 x6 . explicit_CRing_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_90c83eb2afcf0bd3e1333be6478589d0a91068596d7e83371bc99af5bfa18d0e with x1, x2, x3, x4, x5, λ x6 x7 : ο . x7 ⟶ c3510.. (c77b5.. x1 x2 x3 x4 x5) (λ x8 . λ x9 x10 : ι → ι → ι . λ x11 x12 . explicit_CRing_with_id x8 x11 x12 x9 x10).

Apply unknownprop_012ca8caa2f09e68def42ddb439cd4e9c3f98b6e2edd38830763ab994ab639cc with x1, x2, x3, x4, x5, λ x6 x7 : ο . explicit_Field x1 x4 x5 x2 x3 ⟶ x7.

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

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

Apply andI with 3f0d0.. x0, c3510.. x0 (λ x1 . λ x2 x3 : ι → ι → ι . λ x4 x5 . explicit_CRing_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