Claim L0: ∀ x0 . Ring x0 ⟶ struct_b_b_e x0

Let x0 of type ι be given.

Assume H0: Ring x0.

Apply H0 with struct_b_b_e x0.

Assume H1: struct_b_b_e x0.

Assume H2: unpack_b_b_e_o x0 (λ x1 . λ x2 x3 : ι → ι → ι . λ x4 . explicit_Ring x1 x4 x2 x3).

The subproof is completed by applying H1.

Apply unknownprop_f8aa78094125b50fb4c2bb67306c535ef34713dd1b79d9c3a86af7333c45e8da with Ring.

The subproof is completed by applying L0.

■

Proofgold Proof