Apply unknownprop_2504c05a08587fe0873ed45685efc417625f0a904281d653d757d643896f9a70 with
λ x0 . ∀ x1 . x1 ∈ int_alt1 ⟶ add_SNo x0 x1 ∈ int_alt1 leaving 2 subgoals.
Let x0 of type ι be given.
Apply unknownprop_2504c05a08587fe0873ed45685efc417625f0a904281d653d757d643896f9a70 with
λ x1 . add_SNo x0 x1 ∈ int_alt1 leaving 2 subgoals.
Let x1 of type ι be given.
Apply unknownprop_c213ff287d87049b1e6a47a232f87c366800922741a9eeadb1d3ac2fbadaf052 with
add_SNo x0 x1.
Apply add_SNo_In_omega with
x0,
x1 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
Let x1 of type ι be given.
Apply add_SNo_com with
x0,
minus_SNo x1,
λ x2 x3 . x3 ∈ int_alt1 leaving 3 subgoals.
Apply ordinal_SNo with
x0.
Apply nat_p_ordinal with
x0.
Apply omega_nat_p with
x0.
The subproof is completed by applying H0.
Apply SNo_minus_SNo with
x1.
Apply ordinal_SNo with
x1.
Apply nat_p_ordinal with
x1.
Apply omega_nat_p with
x1.
The subproof is completed by applying H1.
Apply unknownprop_6c976be5ae7c4eec61e1190f4b65a1cc39ebfb81542ae63578b69be42c01a06a with
x1,
x0 leaving 2 subgoals.
The subproof is completed by applying H1.
Apply omega_nat_p with
x0.
The subproof is completed by applying H0.
Let x0 of type ι be given.
Apply unknownprop_2504c05a08587fe0873ed45685efc417625f0a904281d653d757d643896f9a70 with
λ x1 . add_SNo (minus_SNo x0) x1 ∈ int_alt1 leaving 2 subgoals.
Let x1 of type ι be given.
Apply unknownprop_6c976be5ae7c4eec61e1190f4b65a1cc39ebfb81542ae63578b69be42c01a06a with
x0,
x1 leaving 2 subgoals.
The subproof is completed by applying H0.
Apply omega_nat_p with
x1.
The subproof is completed by applying H1.
Let x1 of type ι be given.
Apply ordinal_SNo with
x0.
Apply nat_p_ordinal with
x0.
Apply omega_nat_p with
x0.
The subproof is completed by applying H0.
Apply ordinal_SNo with
x1.
Apply nat_p_ordinal with
x1.
Apply omega_nat_p with
x1.
The subproof is completed by applying H1.
Apply minus_add_SNo_distr with
x0,
x1,
λ x2 x3 . x2 ∈ int_alt1 leaving 3 subgoals.
The subproof is completed by applying L2.
The subproof is completed by applying L3.
Apply unknownprop_a66fb27a7b2af57722c6537d3983b55a12cc28475f1d8b8d9bdb1d857010e7af with
add_SNo x0 x1.
Apply add_SNo_In_omega with
x0,
x1 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.