Let x0 of type ι be given.
Let x1 of type ι be given.
Apply unknownprop_4baecc2e952eca39e113b57c19da93bc100e0ff2aac6866a57ba8ff1e36c9807 with
x0,
minus_SNo x1,
λ x2 x3 . x3 = add_SNo ((λ x4 . mul_SNo x4 x4) x0) (add_SNo (minus_SNo (mul_SNo 2 (mul_SNo x0 x1))) ((λ x4 . mul_SNo x4 x4) x1)) leaving 3 subgoals.
The subproof is completed by applying H0.
Apply SNo_minus_SNo with
x1.
The subproof is completed by applying H1.
Let x3 of type ι → ο be given.
Let x5 of type ι → ο be given.
Apply mul_SNo_minus_distrR with
y2,
x3,
λ x6 x7 . mul_SNo 2 x7 = minus_SNo (mul_SNo 2 (mul_SNo y2 x3)),
λ x6 x7 . (λ x8 . x5) (add_SNo x6 ((λ x8 . mul_SNo x8 x8) (minus_SNo x3))) (add_SNo x7 ((λ x8 . mul_SNo x8 x8) (minus_SNo x3))) leaving 4 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
Apply mul_SNo_minus_distrR with
2,
mul_SNo y2 x3 leaving 2 subgoals.
The subproof is completed by applying SNo_2.
Apply SNo_mul_SNo with
y2,
x3 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
Apply unknownprop_355647d7ca15e734de667b76fd2ab30d9dcc30aa55f2f19513d38b4737019c82 with
x3,
λ x6 x7 . (λ x8 . x5) (add_SNo (minus_SNo (mul_SNo 2 (mul_SNo y2 x3))) x6) (add_SNo (minus_SNo (mul_SNo 2 (mul_SNo y2 x3))) x7) leaving 2 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
Apply L2 with
λ x6 . y5 x6 y4 ⟶ y5 y4 x6.
Assume H3: y5 y4 y4.
The subproof is completed by applying H3.
Let x3 of type ι → ι → ο be given.
Apply L2 with
λ x4 . x3 x4 y2 ⟶ x3 y2 x4.
Assume H3: x3 y2 y2.
The subproof is completed by applying H3.