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.
Let x8 of type ι → ι → ι → ι be given.
Let x9 of type ι → ι → ι → ι be given.
Let x10 of type ι → ι → ι be given.
Let x11 of type ι → ι → ι be given.
Let x12 of type ι → ι → ι be given.
Let x13 of type ι → ι → ι be given.
Apply unknownprop_5ceb8947b687470b8a869850421d6b4843b70db05b8766501f5c9a258e737718 with
λ x14 x15 : ι → (ι → ι → ι) → (ι → ι → ι) → (ι → ι → ι) → ι → (ι → ι → ι) → (ι → ι → ι → ι) → (ι → ι → ι) → (ι → ι → ι → ι) → (ι → ι → ι → ι) → (ι → ι → ι) → (ι → ι → ι) → (ι → ι → ι) → (ι → ι → ι) → ο . x15 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 ⟶ ∀ x16 : ο . (Loop_with_defs x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 ⟶ (∃ x17 . and (In x17 x0) (∃ x18 . and (In x18 x0) (∃ x19 . and (In x19 x0) (∃ x20 . and (In x20 x0) (∃ x21 . and (In x21 x0) (not (x6 x21 (x1 (x3 x4 x17) (x9 x18 x19 x17)) x20 = x4))))))) ⟶ x16) ⟶ x16.
The subproof is completed by applying andE with
Loop_with_defs x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13,
∃ x14 . and (In x14 x0) (∃ x15 . and (In x15 x0) (∃ x16 . and (In x16 x0) (∃ x17 . and (In x17 x0) (∃ x18 . and (In x18 x0) (not (x6 x18 (x1 (x3 x4 x14) (x9 x15 x16 x14)) x17 = x4)))))).