Let x0 of type ι be given.
Apply H0 with
∀ x1 . nat_p x1 ⟶ exactly1of2 (odd_nat x1) (odd_nat (add_nat x0 x1)).
Assume H2:
∀ x1 . x1 ∈ omega ⟶ x0 = mul_nat 2 x1 ⟶ ∀ x2 : ο . x2.
Apply nat_ind with
λ x1 . exactly1of2 (odd_nat x1) (odd_nat (add_nat x0 x1)) leaving 2 subgoals.
Apply add_nat_0R with
x0,
λ x1 x2 . exactly1of2 (odd_nat 0) (odd_nat x2).
Apply exactly1of2_I2 with
odd_nat 0,
odd_nat x0 leaving 2 subgoals.
The subproof is completed by applying not_odd_nat_0.
The subproof is completed by applying H0.
Let x1 of type ι be given.
Apply add_nat_SR with
x0,
x1,
λ x2 x3 . exactly1of2 (odd_nat (ordsucc x1)) (odd_nat x3) leaving 2 subgoals.
The subproof is completed by applying H3.
Apply exactly1of2_E with
odd_nat x1,
odd_nat (add_nat x0 x1),
exactly1of2 (odd_nat (ordsucc x1)) (odd_nat (ordsucc (add_nat x0 x1))) leaving 3 subgoals.
The subproof is completed by applying H4.
Apply exactly1of2_I2 with
odd_nat (ordsucc x1),
odd_nat (ordsucc (add_nat x0 x1)) leaving 2 subgoals.
Apply even_nat_not_odd_nat with
ordsucc x1.
Apply odd_nat_even_nat_S with
x1.
The subproof is completed by applying H5.
Apply even_nat_odd_nat_S with
add_nat x0 x1.
Apply even_nat_or_odd_nat with
add_nat x0 x1,
even_nat (add_nat x0 x1) leaving 3 subgoals.
Apply add_nat_p with
x0,
x1 leaving 2 subgoals.
Apply omega_nat_p with
x0.
The subproof is completed by applying H1.
The subproof is completed by applying H3.
The subproof is completed by applying H7.
Apply FalseE with
even_nat (add_nat x0 x1).
Apply H6.
The subproof is completed by applying H7.
Apply exactly1of2_I1 with
odd_nat (ordsucc x1),
odd_nat (ordsucc (add_nat x0 x1)) leaving 2 subgoals.
Apply even_nat_odd_nat_S with
x1.
Apply even_nat_or_odd_nat with
x1,
even_nat x1 leaving 3 subgoals.
The subproof is completed by applying H3.
The subproof is completed by applying H7.
Apply FalseE with
even_nat x1.
Apply H5.
The subproof is completed by applying H7.
Apply even_nat_not_odd_nat with
ordsucc (add_nat x0 x1).
Apply odd_nat_even_nat_S with
add_nat x0 x1.
The subproof is completed by applying H6.