Proofgold Proof

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