Assume H0: ∀ x0 : ι → ι → ο . ∀ x1 : ι → ι → ι . ∀ x2 x3 : ι → ο . ∀ x4 : ι → ι . ∀ x5 x6 x7 . x4 (x1 (x1 (x1 (x1 (x1 (x1 x6 x5) (x1 (x1 (x1 x6 x5) (x1 x7 (x1 (x1 (x1 x5 x5) (x1 (x1 (x1 (x1 x5 (x1 (x1 x6 (x1 x5 (x1 x5 x7))) x5)) x7) (x1 (x4 x6) x7)) (x1 (x1 (x1 (x1 x5 (x4 (x1 x7 x5))) (x1 x6 x6)) (x1 x6 (x1 x7 x5))) x5))) x7))) x5)) x6) (x1 x6 (x1 x5 (x1 (x1 (x4 x5) (x1 (x1 x6 x6) x6)) x5)))) (x4 (x4 x6))) x5) = x4 (x4 x7).
The subproof is completed by applying H0 with
λ x0 x1 . False,
λ x0 x1 . 0,
λ x0 . False,
λ x0 . False,
λ x0 . x0,
0,
0,
Power 0.
Apply FalseE.
Apply unknownprop_03947e47f83a9d5e72cb98dd3f209204911913d012cc97eaa0c7893a771d889d.
The subproof is completed by applying L1.