Proofgold Proof

pf

Let x0 of type ι be given.

Assume H0: CRing_with_id x0.

Apply H0 with explicit_CRing_with_id (K_field_0 x0 x0) (K_field_3 x0 x0) (K_field_4 x0 x0) (K_field_1_b x0 x0) (K_field_2_b x0 x0).

Assume H1: struct_b_b_e_e x0.

Apply unknownprop_50ae0d1c45204b46a4fcc7a6bee445594122c11b111b42c080baae0465265b26 with x0, λ x1 x2 . unpack_b_b_e_e_o x2 (λ x3 . λ x4 x5 : ι → ι → ι . λ x6 x7 . explicit_CRing_with_id x3 x6 x7 x4 x5) ⟶ explicit_CRing_with_id (K_field_0 x0 x0) (K_field_3 x0 x0) (K_field_4 x0 x0) (K_field_1_b x0 x0) (K_field_2_b x0 x0) leaving 2 subgoals.

The subproof is completed by applying H0.

Apply CRing_with_id_unpack_eq with K_field_0 x0 x0, K_field_1_b x0 x0, K_field_2_b x0 x0, K_field_3 x0 x0, K_field_4 x0 x0, λ x1 x2 : ο . x2 ⟶ explicit_CRing_with_id (K_field_0 x0 x0) (K_field_3 x0 x0) (K_field_4 x0 x0) (K_field_1_b x0 x0) (K_field_2_b x0 x0).

Assume H2: explicit_CRing_with_id (K_field_0 x0 x0) (K_field_3 x0 x0) (K_field_4 x0 x0) (K_field_1_b x0 x0) (K_field_2_b x0 x0).

The subproof is completed by applying H2.

■