Let x0 of type ι be given.
Let x1 of type ι → ο be given.
Let x2 of type ι be given.
Assume H1: x1 x2.
Claim L2:
∃ x3 . and (In x3 x0) (x1 x3)Let x3 of type ο be given.
Assume H2:
∀ x4 . and (In x4 x0) (x1 x4) ⟶ x3.
Apply H2 with
x2.
Apply unknownprop_389e2fb1855352fcc964ea44fe6723d7a1c2d512f04685300e3e97621725b977 with
In x2 x0,
x1 x2 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
Apply unknownprop_cd9802cfa8b6e6a33231f7ea81630a8af696519ed87942920eb067471609b68b with
λ x3 x4 : ι → (ι → ο) → ι . In x2 (x4 x0 (λ x5 . x1 x5)).
Apply unknownprop_6f44febdf8a865ee94133af873e3c2941a931de6ac80968301360290e02ca608 with
∃ 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.
The subproof is completed by applying L2.
Apply L3 with
λ x3 x4 . In x2 x4.
Claim L4:
(λ x3 . If_i (x1 x3) x3 (Eps_i (λ x4 . and (In x4 x0) (x1 x4)))) x2 = x2Apply unknownprop_6f44febdf8a865ee94133af873e3c2941a931de6ac80968301360290e02ca608 with
x1 x2,
x2,
Eps_i (λ x3 . and (In x3 x0) (x1 x3)).
The subproof is completed by applying H1.
Apply L4 with
λ x3 x4 . In x3 (Repl x0 (λ x5 . (λ x6 . If_i (x1 x6) x6 (Eps_i (λ x7 . and (In x7 x0) (x1 x7)))) x5)).
Apply unknownprop_63c308b92260dbfca8c9530846e6836ba3e6be221cc8e80fd61db913e01bdacf with
x0,
λ x3 . If_i (x1 x3) x3 (Eps_i (λ x4 . and (In x4 x0) (x1 x4))),
x2.
The subproof is completed by applying H0.