Let x0 of type ι be given.
Let x1 of type ι be given.
Assume H0: x0 ∈ 2.
Assume H1: x1 ∈ 2.
Assume H2: x0 = x1 ⟶ ∀ x2 : ο . x2.
Apply PigeonHole_nat_bij with
2,
λ x2 . ap (lam 2 (λ x3 . If_i (x3 = 0) x0 x1)) x2 leaving 3 subgoals.
The subproof is completed by applying nat_2.
Let x2 of type ι be given.
Assume H3: x2 ∈ 2.
Apply cases_2 with
x2,
λ x3 . ap (lam 2 (λ x4 . If_i (x4 = 0) x0 x1)) x3 ∈ 2 leaving 3 subgoals.
The subproof is completed by applying H3.
Apply tuple_2_0_eq with
x0,
x1,
λ x3 x4 . x4 ∈ 2.
The subproof is completed by applying H0.
Apply tuple_2_1_eq with
x0,
x1,
λ x3 x4 . x4 ∈ 2.
The subproof is completed by applying H1.
Let x2 of type ι be given.
Assume H3: x2 ∈ 2.
Let x3 of type ι be given.
Assume H4: x3 ∈ 2.
Apply cases_2 with
x2,
λ x4 . ap (lam 2 (λ x5 . If_i (x5 = 0) x0 x1)) x4 = ap (lam 2 (λ x5 . If_i (x5 = 0) x0 x1)) x3 ⟶ x4 = x3 leaving 3 subgoals.
The subproof is completed by applying H3.
Apply cases_2 with
x3,
λ x4 . ap (lam 2 (λ x5 . If_i (x5 = 0) x0 x1)) 0 = ap (lam 2 (λ x5 . If_i (x5 = 0) x0 x1)) x4 ⟶ 0 = x4 leaving 3 subgoals.
The subproof is completed by applying H4.
Assume H5:
ap (lam 2 (λ x4 . If_i (x4 = 0) x0 x1)) 0 = ap (lam 2 (λ x4 . If_i (x4 = 0) x0 x1)) 0.
Let x4 of type ι → ι → ο be given.
Assume H6: x4 0 0.
The subproof is completed by applying H6.
Apply tuple_2_0_eq with
x0,
x1,
λ x4 x5 . (λ x6 . x5 = ap (lam 2 (λ x7 . If_i (x7 = 0) x0 x1)) x6 ⟶ 0 = x6) 1.
Apply tuple_2_1_eq with
x0,
x1,
λ x4 x5 . x0 = x5 ⟶ 0 = 1.
Assume H5: x0 = x1.
Apply H2 with
0 = 1.
The subproof is completed by applying H5.
Apply cases_2 with
x3,
λ x4 . ap (lam 2 (λ x5 . If_i (x5 = 0) x0 x1)) 1 = ap (lam 2 (λ x5 . If_i (x5 = 0) x0 x1)) x4 ⟶ 1 = x4 leaving 3 subgoals.
The subproof is completed by applying H4.
Apply tuple_2_1_eq with
x0,
x1,
λ x4 x5 . (λ x6 . x5 = ap (lam 2 (λ x7 . If_i (x7 = 0) x0 x1)) x6 ⟶ 1 = x6) 0.
Apply tuple_2_0_eq with
x0,
x1,
λ x4 x5 . x1 = x5 ⟶ 1 = 0.
Assume H5: x1 = x0.
Apply H2 with
1 = 0.
Let x4 of type ι → ι → ο be given.
The subproof is completed by applying H5 with λ x5 x6 . x4 x6 x5.
Assume H5:
ap (lam 2 (λ x4 . If_i (x4 = 0) x0 x1)) 1 = ap (lam 2 (λ x4 . If_i ... ... ...)) 1.