Let x0 of type ι be given.
Let x1 of type ι → ι be given.
Let x2 of type ι be given.
Apply unknownprop_99c6830b7507eb1c538c7366f637e956be6dad337531dd2702ca6ba6923a9849 with
Repl x0 (λ x3 . x1 x3),
x2,
∃ x3 . and (In x3 x0) (In x2 (x1 x3)) leaving 2 subgoals.
Apply unknownprop_0bc1e6c77e36f428b4f8a3657d1f006ea28b568ebe9c995e5a7c18b75045b2a3 with
λ x3 x4 : ι → (ι → ι) → ι . In x2 (x3 x0 x1).
The subproof is completed by applying H0.
Let x3 of type ι be given.
Assume H2:
In x3 (Repl x0 (λ x4 . x1 x4)).
Apply unknownprop_89e422bb3b8a01dd209d7f2f210df650a435fc3e6005e0f59c57a5e7a59a6d0e with
x0,
x1,
x3,
∃ x4 . and (In x4 x0) (In x2 (x1 x4)) leaving 2 subgoals.
The subproof is completed by applying H2.
Let x4 of type ι be given.
Assume H4: x3 = x1 x4.
Let x5 of type ο be given.
Assume H5:
∀ x6 . and (In x6 x0) (In x2 (x1 x6)) ⟶ x5.
Apply H5 with
x4.
Apply unknownprop_389e2fb1855352fcc964ea44fe6723d7a1c2d512f04685300e3e97621725b977 with
In x4 x0,
In x2 (x1 x4) leaving 2 subgoals.
The subproof is completed by applying H3.
Apply H4 with
λ x6 x7 . In x2 x6.
The subproof is completed by applying H1.