leaving 2 subgoals.
Let x0 of type ι be given.
Assume H1:
∀ x1 : ι → ι . (∀ x2 . x2 ∈ x0 ⟶ nat_p (x1 x2)) ⟶ nat_p (Sigma_nat x0 x1).
Let x1 of type ι → ι be given.
Apply unknownprop_32bc7778cd02b216f957f8c5e9693c4b58b7ca04a4ca47b5f3adb522add7dd35 with
x0,
x1,
λ x2 x3 . nat_p x3 leaving 2 subgoals.
The subproof is completed by applying H0.
Apply add_nat_p with
Sigma_nat x0 x1,
x1 x0 leaving 2 subgoals.
Apply H1 with
x1.
Let x2 of type ι be given.
Assume H3: x2 ∈ x0.
Apply H2 with
x2.
Apply ordsuccI1 with
x0,
x2.
The subproof is completed by applying H3.
Apply H2 with
x0.
The subproof is completed by applying ordsuccI2 with x0.