Proofgold Proof

pf
Claim L0: ∀ x0 . Group x0 ⟶ struct_b x0 Let x0 of type ι be given. Assume H0: Group x0. Apply H0 with struct_b x0. Assume H1: struct_b x0. Assume H2: unpack_b_o x0 explicit_Group. The subproof is completed by applying H1. Apply unknownprop_be2503b86c1e5792746c6adc58383e3972a7c1b0d953c88e847e4de130b06873 with Group. The subproof is completed by applying L0. ■