Proofgold Proof

pf
Let x0 of type ι be given. Assume H0: odd_nat x0. Apply unknownprop_c22c9b7977d51762c26ddf3ddc641cbcb61926912ae1225d39df1b293afb8250 with x0, x0 leaving 2 subgoals. The subproof is completed by applying H0. The subproof is completed by applying H0. ■