Proofgold Proof

pf

Let x0 of type ι be given.

Assume H0: Field x0.

Apply H0 with x0 = pack_b_b_e_e (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).

Assume H1: struct_b_b_e_e x0.

Assume H2: unpack_b_b_e_e_o x0 (λ x1 . λ x2 x3 : ι → ι → ι . λ x4 x5 . explicit_Field x1 x4 x5 x2 x3).

Apply struct_b_b_e_e_eta with x0.

The subproof is completed by applying H1.

■