Proofgold Proof

pf
Apply set_ext with 4ae4a.. (4ae4a.. 4a7ef..), prim2 4a7ef.. (4ae4a.. 4a7ef..) leaving 2 subgoals. The subproof is completed by applying unknownprop_a099319a1ba0bd8a8c96ec49e0625dd923e73a0ca3eb2f9fadbdc2d9d4b34480. The subproof is completed by applying unknownprop_be46613bed5044fc8a5bc3e9fe143742429d2b31191f0244d470d6a5bb9af78c. ■