Let x0 of type ι be given.
Let x1 of type ι → ο be given.
Let x2 of type ι be given.
Apply unknownprop_cd9802cfa8b6e6a33231f7ea81630a8af696519ed87942920eb067471609b68b with
λ x3 x4 : ι → (ι → ο) → ι . In x2 (x4 x0 (λ x5 . x1 x5)) ⟶ and (In x2 x0) (x1 x2).
Apply unknownprop_b257b354d80b58d9a8444b167a21f47b4aabc910dc3698404491d5ef01e18cf3 with
∃ x3 . and (In x3 x0) (x1 x3),
In x2 (If_i (∃ x3 . and (In x3 x0) (x1 x3)) (Repl x0 (λ x3 . (λ x4 . If_i (x1 x4) x4 (Eps_i (λ x5 . and (In x5 x0) (x1 x5)))) x3)) 0) ⟶ and (In x2 x0) (x1 x2) leaving 2 subgoals.
Assume H0:
∃ x3 . and (In x3 x0) (x1 x3).
Claim L1:
If_i (∃ x3 . and (In x3 x0) (x1 x3)) (Repl x0 (λ x3 . (λ x4 . If_i (x1 x4) x4 (Eps_i (λ x5 . and (In x5 x0) (x1 x5)))) x3)) 0 = Repl x0 (λ x3 . (λ x4 . If_i (x1 ...) ... ...) ...)Apply L1 with
λ x3 x4 . In x2 x4 ⟶ and (In x2 x0) (x1 x2).
Assume H2:
In x2 (Repl x0 (λ x3 . (λ x4 . If_i (x1 x4) x4 (Eps_i (λ x5 . and (In x5 x0) (x1 x5)))) x3)).
Apply unknownprop_89e422bb3b8a01dd209d7f2f210df650a435fc3e6005e0f59c57a5e7a59a6d0e with
x0,
λ x3 . If_i (x1 x3) x3 (Eps_i (λ x4 . and (In x4 x0) (x1 x4))),
x2,
and (In x2 x0) (x1 x2) leaving 2 subgoals.
The subproof is completed by applying H2.
Let x3 of type ι be given.
Assume H4:
x2 = (λ x4 . If_i (x1 x4) x4 (Eps_i (λ x5 . and (In x5 x0) (x1 x5)))) x3.
Apply unknownprop_b257b354d80b58d9a8444b167a21f47b4aabc910dc3698404491d5ef01e18cf3 with
x1 x3,
and (In x2 x0) (x1 x2) leaving 2 subgoals.
Assume H5: x1 x3.
Claim L6: x2 = x3
Apply unknownprop_6f44febdf8a865ee94133af873e3c2941a931de6ac80968301360290e02ca608 with
x1 x3,
x3,
Eps_i (λ x4 . and (In x4 x0) (x1 x4)),
λ x4 x5 . x2 = x4 leaving 2 subgoals.
The subproof is completed by applying H5.
The subproof is completed by applying H4.
Apply L6 with
λ x4 x5 . and (In x5 x0) (x1 x5).
Apply unknownprop_389e2fb1855352fcc964ea44fe6723d7a1c2d512f04685300e3e97621725b977 with
In x3 x0,
x1 x3 leaving 2 subgoals.
The subproof is completed by applying H3.
The subproof is completed by applying H5.
Claim L6:
x2 = Eps_i (λ x4 . and (In x4 x0) (x1 x4))Apply unknownprop_5a150bd86f4285de5d98c60b17d4452a655b4d88de0a02247259cdad6e6d992c with
x1 x3,
x3,
Eps_i (λ x4 . and (In x4 x0) (x1 x4)),
λ x4 x5 . x2 = x4 leaving 2 subgoals.
The subproof is completed by applying H5.
The subproof is completed by applying H4.
Apply L6 with
λ x4 x5 . and (In x5 x0) (x1 x5).
Apply Eps_i_ex with
λ x4 . and (In x4 x0) (x1 x4).
The subproof is completed by applying H0.