Let x0 of type ι be given.
Let x1 of type ι → ο be given.
Let x2 of type ι be given.
Assume H0: x2 ∈ x0.
Assume H1: x1 x2.
Claim L2:
∃ x3 . and (x3 ∈ x0) (x1 x3)Let x3 of type ο be given.
Assume H2:
∀ x4 . and (x4 ∈ x0) (x1 x4) ⟶ x3.
Apply H2 with
x2.
Apply andI with
x2 ∈ x0,
x1 x2 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
Claim L3:
If_i (∃ x3 . and (x3 ∈ x0) (x1 x3)) {(λ x4 . If_i (x1 x4) x4 (prim0 (λ x5 . and (x5 ∈ x0) (x1 x5)))) x3|x3 ∈ x0} 0 = {(λ x4 . If_i (x1 x4) x4 (prim0 (λ x5 . and (x5 ∈ x0) (x1 x5)))) x3|x3 ∈ x0}Apply If_i_1 with
∃ x3 . and (x3 ∈ x0) (x1 x3),
{(λ x4 . If_i (x1 x4) x4 (prim0 (λ x5 . and (x5 ∈ x0) (x1 x5)))) x3|x3 ∈ x0},
0.
The subproof is completed by applying L2.
Apply L3 with
λ x3 x4 . x2 ∈ x4.
Claim L4:
(λ x3 . If_i (x1 x3) x3 (prim0 (λ x4 . and (x4 ∈ x0) (x1 x4)))) x2 = x2Apply If_i_1 with
x1 x2,
x2,
prim0 (λ x3 . and (x3 ∈ x0) (x1 x3)).
The subproof is completed by applying H1.
Apply L4 with
λ x3 x4 . x3 ∈ {(λ x6 . If_i (x1 x6) x6 (prim0 (λ x7 . and (x7 ∈ x0) (x1 x7)))) x5|x5 ∈ x0}.
Apply ReplI with
x0,
λ x3 . If_i (x1 x3) x3 (prim0 (λ x4 . and (x4 ∈ x0) (x1 x4))),
x2.
The subproof is completed by applying H0.