Let x0 of type ι be given.
Assume H1: x0 = 0 ⟶ ∀ x1 : ο . x1.
set y1 to be ...
set y2 to be 1
Claim L14: ∀ x3 : ι → ο . x3 y2 ⟶ x3 y1
Let x3 of type ι → ο be given.
Assume H14: x3 1.
set y4 to be ...
set y5 to be ...
Claim L15: ∀ x6 : ι → ο . x6 y5 ⟶ x6 y4
Let x6 of type ι → ο be given.
set y7 to be ...
set y6 to be λ x6 . y5
Apply L15 with
λ x7 . y6 x7 y5 ⟶ y6 y5 x7 leaving 2 subgoals.
Assume H16: y6 y5 y5.
The subproof is completed by applying H16.
Apply CSNo_relative_recip with
y5,
recip_SNo (add_SNo (exp_SNo_nat (CSNo_Re y5) 2) (exp_SNo_nat (CSNo_Im y5) 2)),
λ x7 . y6 leaving 4 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying L7.
The subproof is completed by applying L15.
Let x3 of type ι → ι → ο be given.
Apply L14 with
λ x4 . x3 x4 y2 ⟶ x3 y2 x4.
Assume H15: x3 y2 y2.
The subproof is completed by applying H15.