Let x0 of type ι be given.
Assume H1: x0 = 0 ⟶ ∀ x1 : ο . x1.
set y1 to be ...
set y2 to be 1
Claim L16: ∀ x3 : ι → ο . x3 y2 ⟶ x3 y1
Let x3 of type ι → ο be given.
Assume H16: x3 1.
set y4 to be ...
set y5 to be ...
Claim L17: ∀ x6 : ι → ο . x6 y5 ⟶ x6 y4
Let x6 of type ι → ο be given.
set y7 to be ...
set y6 to be λ x6 . y5
Apply L17 with
λ x7 . y6 x7 y5 ⟶ y6 y5 x7 leaving 2 subgoals.
Assume H18: y6 y5 y5.
The subproof is completed by applying H18.
Apply unknownprop_0d97a0552c8901c8e5c1ff922af7643b21490c8f0cb217a138610332491bad62 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 L9.
The subproof is completed by applying L17.
Let x3 of type ι → ι → ο be given.
Apply L16 with
λ x4 . x3 x4 y2 ⟶ x3 y2 x4.
Assume H17: x3 y2 y2.
The subproof is completed by applying H17.