Let x0 of type ι be given.
Assume H0: x0 ∈ 3.
Let x1 of type ι be given.
Assume H1: x1 ∈ 3.
Assume H2: x0 = x1 ⟶ ∀ x2 : ο . x2.
Apply cases_3 with
x0,
λ x2 . x0 = x2 ⟶ ∃ x3 . and (x3 ∈ 3) (∀ x4 . x4 ∈ 3 ⟶ (x4 = x3 ⟶ ∀ x5 : ο . x5) ⟶ or (x4 = x2) (x4 = x1)) leaving 5 subgoals.
The subproof is completed by applying H0.
Assume H3: x0 = 0.
Apply cases_3 with
x1,
λ x2 . x1 = x2 ⟶ ∃ x3 . and (x3 ∈ 3) (∀ x4 . x4 ∈ 3 ⟶ (x4 = x3 ⟶ ∀ x5 : ο . x5) ⟶ or (x4 = 0) (x4 = x2)) leaving 5 subgoals.
The subproof is completed by applying H1.
Assume H4: x1 = 0.
Apply FalseE with
∃ x2 . and (x2 ∈ 3) (∀ x3 . x3 ∈ 3 ⟶ (x3 = x2 ⟶ ∀ x4 : ο . x4) ⟶ or (x3 = 0) (x3 = 0)).
Apply H2.
Apply H4 with
λ x2 x3 . x0 = x3.
The subproof is completed by applying H3.
Assume H4: x1 = 1.
Let x2 of type ο be given.
Assume H5:
∀ x3 . and (x3 ∈ 3) (∀ x4 . x4 ∈ 3 ⟶ (x4 = x3 ⟶ ∀ x5 : ο . x5) ⟶ or (x4 = 0) (x4 = 1)) ⟶ x2.
Apply H5 with
2.
Apply andI with
2 ∈ 3,
∀ x3 . x3 ∈ 3 ⟶ (x3 = 2 ⟶ ∀ x4 : ο . x4) ⟶ or (x3 = 0) (x3 = 1) leaving 2 subgoals.
The subproof is completed by applying In_2_3.
Let x3 of type ι be given.
Assume H6: x3 ∈ 3.
Apply cases_3 with
x3,
λ x4 . (x4 = 2 ⟶ ∀ x5 : ο . x5) ⟶ or (x4 = 0) (x4 = 1) leaving 4 subgoals.
The subproof is completed by applying H6.
Assume H7: 0 = 2 ⟶ ∀ x4 : ο . x4.
Apply orIL with
0 = 0,
0 = 1.
Let x4 of type ι → ι → ο be given.
Assume H8: x4 0 0.
The subproof is completed by applying H8.
Assume H7: 1 = 2 ⟶ ∀ x4 : ο . x4.
Apply orIR with
1 = 0,
1 = 1.
Let x4 of type ι → ι → ο be given.
Assume H8: x4 1 1.
The subproof is completed by applying H8.
Assume H7: 2 = 2 ⟶ ∀ x4 : ο . x4.
Apply FalseE with
or (2 = 0) (2 = 1).
Apply H7.
Let x4 of type ι → ι → ο be given.
Assume H8: x4 2 2.
The subproof is completed by applying H8.
Assume H4: x1 = 2.
Let x2 of type ο be given.
Assume H5:
∀ x3 . and (x3 ∈ 3) (∀ x4 . x4 ∈ 3 ⟶ (x4 = x3 ⟶ ∀ x5 : ο . x5) ⟶ or (x4 = 0) (x4 = 2)) ⟶ x2.
Apply H5 with
1.
Apply andI with
1 ∈ 3,
∀ x3 . x3 ∈ 3 ⟶ (x3 = 1 ⟶ ∀ x4 : ο . x4) ⟶ or (x3 = 0) (x3 = 2) leaving 2 subgoals.
The subproof is completed by applying In_1_3.
Let x3 of type ι be given.
Assume H6: x3 ∈ 3.
Apply cases_3 with
x3,
λ x4 . (... = 1 ⟶ ∀ x5 : ο . x5) ⟶ or (x4 = 0) (x4 = 2) leaving 4 subgoals.