Proofgold Proof

pf
Apply unknownprop_c7aff8a258081ead27bbcfd1253378c01beaa0edda67f8a38bea5872be2d604f 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. ■