Proofgold Proof

pf
Apply nat_trans with u17, u12 leaving 2 subgoals. The subproof is completed by applying nat_17. The subproof is completed by applying unknownprop_b7a4a37161804b376f25028de76b0714142123cbd842ba90c86afe8baa6a8a9e. ■