Proofgold Proof

pf
Let x0 of type ι be given. Let x1 of type ι be given. Assume H0: nat_p x1. Apply unknownprop_4e3b33b1166f6152a39a44a865c600b0b9f1dfa87f521be03670a83f1d10a167 with 1, λ x2 x3 . mul_nat x0 x3, x1. The subproof is completed by applying H0. ■