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 : ι → (ι → ι → ι) → (ι → ι → ι) → (ι → ι → ι) → ι → (ι → ι → ι) → (ι → ι → ι → ι) → (ι → ι → ι) → (ι → ι → ι → ι) → (ι → ι → ι → ι) → (ι → ι → ι) → (ι → ι → ι) → (ι → ι → ι) → (ι → ι → ι) → ο . Loop_with_defs x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 ⟶ (∃ x16 . and (In x16 x0) (∃ x17 . and (In x17 x0) (∃ x18 . and (In x18 x0) (∃ x19 . and (In x19 x0) (∃ x20 . and (In x20 x0) (not (x6 x20 (x1 (x3 x4 x16) (x9 x17 x18 x16)) x19 = x4))))))) ⟶ x15 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13.
The subproof is completed by applying unknownprop_389e2fb1855352fcc964ea44fe6723d7a1c2d512f04685300e3e97621725b977 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)))))).