Let x0 of type ι be given.
Let x1 of type ι → ι be given.
Apply nat_ind with
λ x2 . and (∀ x3 . x3 ∈ ap (SNo_recipaux x0 x1 x2) 0 ⟶ and (SNo x3) (SNoLt (mul_SNo x0 x3) 1)) (∀ x3 . x3 ∈ ap (SNo_recipaux x0 x1 x2) 1 ⟶ and (SNo x3) (SNoLt 1 (mul_SNo x0 x3))) leaving 2 subgoals.
Apply andI with
∀ x2 . x2 ∈ ap (SNo_recipaux x0 x1 0) 0 ⟶ and (SNo x2) (SNoLt (mul_SNo x0 x2) 1),
∀ x2 . x2 ∈ ap (SNo_recipaux x0 x1 0) 1 ⟶ and (SNo x2) (SNoLt 1 (mul_SNo x0 x2)) leaving 2 subgoals.
Let x2 of type ι be given.
Apply SNo_recipaux_0 with
x0,
x1,
λ x3 x4 . x2 ∈ ap x4 0 ⟶ and (SNo x2) (SNoLt (mul_SNo x0 x2) 1).
Apply tuple_2_0_eq with
Sing 0,
0,
λ x3 x4 . x2 ∈ x4 ⟶ and (SNo x2) (SNoLt (mul_SNo x0 x2) 1).
Apply SingE with
0,
x2,
λ x3 x4 . and (SNo x4) (SNoLt (mul_SNo x0 x4) 1) leaving 2 subgoals.
The subproof is completed by applying H5.
Apply andI with
SNo 0,
SNoLt (mul_SNo x0 0) 1 leaving 2 subgoals.
The subproof is completed by applying SNo_0.
Apply mul_SNo_zeroR with
x0,
λ x3 x4 . SNoLt x4 1 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying SNoLt_0_1.
Let x2 of type ι be given.
Apply SNo_recipaux_0 with
x0,
x1,
λ x3 x4 . x2 ∈ ap x4 1 ⟶ and (SNo x2) (SNoLt 1 (mul_SNo x0 x2)).
Apply tuple_2_1_eq with
Sing 0,
0,
λ x3 x4 . x2 ∈ x4 ⟶ and (SNo x2) (SNoLt 1 (mul_SNo x0 x2)).
Assume H5: x2 ∈ 0.
Apply FalseE with
and (SNo x2) (SNoLt 1 (mul_SNo x0 x2)).
Apply EmptyE with
x2.
The subproof is completed by applying H5.
Let x2 of type ι be given.