Proofgold Proof

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