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_5ef6db00f3c15a86c1e221d4a4c3ce606c4d873a1f90dd0b36114bf603c362c9 with Group. The subproof is completed by applying L0. ■