Proofgold Proof

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