Let x0 of type ι be given.
Apply exp_SNo_nat_S with
x0,
1,
λ x1 x2 . x2 = mul_SNo x0 x0 leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying nat_1.
Claim L1: ∀ x3 : ι → ο . x3 y2 ⟶ x3 y1
Let x3 of type ι → ο be given.
set y4 to be λ x4 . x3
Apply exp_SNo_nat_1 with
y2,
λ x5 x6 . y4 (mul_SNo y2 x5) (mul_SNo y2 x6) leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
Let x3 of type ι → ι → ο be given.
Apply L1 with
λ x4 . x3 x4 y2 ⟶ x3 y2 x4.
Assume H2: x3 y2 y2.
The subproof is completed by applying H2.