Let x0 of type ι be given.
Let x1 of type ι be given.
Apply add_nat_com with
x1,
x0,
λ x2 x3 . or (x1 = 0) (x0 ∈ x3) 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.