Proofgold Proof

pf
Apply unknownprop_d576838b332114c90b2af560b99977995a2da890fc52757cf56c82a16d1c86c8 with struct_b_b_e_e. Let x0 of type ι be given. Assume H0: struct_b_b_e_e x0. The subproof is completed by applying H0. ■