Proofgold Proof

pf
Apply unknownprop_4da5fc600f2b33aedc274a99663b5b8b863d740d1d214334be4061845214dfc3 with λ x0 x1 . nat_p x0. Apply add_nat_p with 16, 8 leaving 2 subgoals. The subproof is completed by applying nat_16. The subproof is completed by applying nat_8. ■