Let x0 of type ι be given.

Assume H0: Field x0.

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

Apply H1 with λ x1 . unpack_b_b_e_e_o x1 (λ x2 . λ x3 x4 : ι → ι → ι . λ x5 x6 . explicit_Field x2 x5 x6 x3 x4) ⟶ unpack_b_b_e_e_o 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 . x3 ∈ x1 ⟶ ∀ x4 . x4 ∈ x1 ⟶ x2 x3 x4 ∈ x1.

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

Assume H3: ∀ x4 . x4 ∈ x1 ⟶ ∀ x5 . x5 ∈ x1 ⟶ x3 x4 x5 ∈ x1.

Let x4 of type ι be given.

Assume H4: x4 ∈ x1.

Let x5 of type ι be given.

Assume H5: x5 ∈ x1.

Apply Field_unpack_eq with x1, x2, x3, x4, x5, λ x6 x7 : ο . x7 ⟶ unpack_b_b_e_e_o (pack_b_b_e_e x1 x2 x3 x4 x5) (λ x8 . λ x9 x10 : ι → ι → ι . λ x11 x12 . explicit_CRing_with_id x8 x11 x12 x9 x10).

Apply CRing_with_id_unpack_eq 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: unpack_b_b_e_e_o x0 (λ x1 . λ x2 x3 : ι → ι → ι . λ x4 x5 . explicit_Field x1 x4 x5 x2 x3).

Apply andI with struct_b_b_e_e x0, unpack_b_b_e_e_o 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