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_c7aff8a258081ead27bbcfd1253378c01beaa0edda67f8a38bea5872be2d604f with Ring.

The subproof is completed by applying L0.

■

Proofgold Proof