Claim L0: ∀ x0 . Ring_with_id x0 ⟶ struct_b_b_e_e x0

Let x0 of type ι be given.

Assume H0: Ring_with_id x0.

Apply H0 with struct_b_b_e_e x0.

Assume H1: struct_b_b_e_e x0.

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

The subproof is completed by applying H1.

Apply unknownprop_d576838b332114c90b2af560b99977995a2da890fc52757cf56c82a16d1c86c8 with Ring_with_id.

The subproof is completed by applying L0.

■

Proofgold Proof