Let x0 of type ι → ο be given.
Let x1 of type ι → ι → ι → ο be given.
Let x2 of type ι → ι be given.
Let x3 of type ι → ι → ι → ι → ι → ι be given.
Let x4 of type ι → ι be given.
Let x5 of type ι → ι → ι → ι be given.
Let x6 of type ι → ι be given.
Let x7 of type ι → ι be given.
The subproof is completed by applying and3E with ∀ x8 . x0 x8 ⟶ x3 (x4 (x4 (x4 x8))) (x4 (x4 x8)) (x4 x8) (x7 x8) (x5 (x4 (x4 x8)) (x4 x8) (x7 x8)) = x3 (x4 (x4 (x4 x8))) (x4 (x4 x8)) (x4 x8) (x7 x8) (x7 (x4 x8)), ∀ x8 . x0 x8 ⟶ x3 (x4 x8) (x4 (x4 x8)) (x4 x8) (x7 x8) (x6 (x4 x8)) = x2 (x4 x8), ∀ x8 . x0 x8 ⟶ x3 (x4 x8) (x4 (x4 x8)) (x4 x8) (x7 x8) (x5 x8 (x4 x8) (x6 x8)) = x2 (x4 x8).