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.
Assume H0: x4 = x3 ⟶ ∀ x5 : ο . x5.
Apply xm with
x4 ∈ x1,
ap (lam x1 (λ x5 . If_i (x5 = x3) x0 (x2 (ordsucc x3) x5))) x4 = ap (lam x1 (λ x5 . x2 (ordsucc x3) x5)) x4 leaving 2 subgoals.
Assume H1: x4 ∈ x1.
Apply beta with
x1,
λ x5 . If_i (x5 = x3) x0 (x2 (ordsucc x3) x5),
x4,
λ x5 x6 . x6 = ap (lam x1 (λ x7 . x2 (ordsucc x3) x7)) x4 leaving 2 subgoals.
The subproof is completed by applying H1.
Apply beta with
x1,
λ x5 . x2 (ordsucc x3) x5,
x4,
λ x5 x6 . If_i (x4 = x3) x0 (x2 (ordsucc x3) x4) = x6 leaving 2 subgoals.
The subproof is completed by applying H1.
Apply If_i_0 with
x4 = x3,
x0,
x2 (ordsucc x3) x4.
The subproof is completed by applying H0.
Assume H1:
not (x4 ∈ x1).
Apply beta0 with
x1,
λ x5 . x2 (ordsucc x3) x5,
x4,
λ x5 x6 . ap (lam x1 (λ x7 . If_i (x7 = x3) x0 (x2 (ordsucc x3) x7))) x4 = x6 leaving 2 subgoals.
The subproof is completed by applying H1.
Apply beta0 with
x1,
λ x5 . If_i (x5 = x3) x0 (x2 (ordsucc x3) x5),
x4.
The subproof is completed by applying H1.