Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Let x1 of type ι be given.
Assume H0: nat_p x0.
Assume H1: nat_p x1.
Assume H2: x0 = add_nat x0 x1.
Apply unknownprop_8e86c83b3f10090834577a21f7b492ac191465dc9eb87a73d3ba817de938dadf with x0, x1 leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
Apply H2 with λ x2 x3 . x2 ⊆ x0.
The subproof is completed by applying Subq_ref with x0.
■