Proofgold Proof

pf
Apply unknownprop_92b7514ef3d0f5b6f05d43c13e9c99120ec6f325219c0abcbb2506a32700bb9b with 2 leaving 2 subgoals. The subproof is completed by applying nat_2. The subproof is completed by applying In_1_2. ■