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_0a2398199d0e661dceb5727c5962513eba79af7107a3baa60eecf32bec618655 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) (not (x5 (x1 (x2 (x8 x17 x18 x16) x4) 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) (not (x5 (x1 (x2 (x8 x15 x16 x14) x4) x14) x17 = x4))))).