Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: nat_p x0.
Let x1 of type ι be given.
Assume H1: nat_p x1.
Apply add_nat_com with x1, x0, λ x2 x3 . or (x1 = 0) (x0x3) leaving 3 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H0.
Apply unknownprop_d40a199c08c77164672e4ca0cbff2f0aefbdc2d634556cb19632c21a32e1558c with x0, x1 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.