---

Step * 1 2 1 1 2 1 of Lemma polymorphic-choice-base


1. f : ⋂A:Type. (A ⟶ A ⟶ A)
2. ∀x,y:Base.  (↓((f x y) = x ∈ Base) ∨ ((f x y) = y ∈ Base))
3. ∀z:Base. ((f z z) = z ∈ Base)
4. ((f 0 1) = 0 ∈ Base) ∨ ((f 0 1) = 1 ∈ Base)
5. 0 = 0 ∈ Base
6. ∀x,y:ℤ.  ((f x y) = x ∈ ℤ)
7. (f 1 0) = 1 ∈ ℤ
8. ∀y:Base. ((f 1 y) = 1 ∈ Base)
9. x : Base
10. (f x 0) = 0 ∈ Base
11. T : Type
12. x = 1 ∈ T
13. 0 = 0 ∈ T
14. (1 = 0 ∈ T) ⇒ (x = 0 ∈ Base)
15. f ∈ T ⟶ T ⟶ T
16. (f 1 0) = (f x 0) ∈ T
⊢ (f x 0) = x ∈ Base
BY
{ (D -3 THENM (HypSubst' (-1) 0 THEN Auto)) }

1
.....antecedent..... 
1. f : ⋂A:Type. (A ⟶ A ⟶ A)
2. ∀x,y:Base.  (↓((f x y) = x ∈ Base) ∨ ((f x y) = y ∈ Base))
3. ∀z:Base. ((f z z) = z ∈ Base)
4. ((f 0 1) = 0 ∈ Base) ∨ ((f 0 1) = 1 ∈ Base)
5. 0 = 0 ∈ Base
6. ∀x,y:ℤ.  ((f x y) = x ∈ ℤ)
7. (f 1 0) = 1 ∈ ℤ
8. ∀y:Base. ((f 1 y) = 1 ∈ Base)
9. x : Base
10. (f x 0) = 0 ∈ Base
11. T : Type
12. x = 1 ∈ T
13. 0 = 0 ∈ T
14. f ∈ T ⟶ T ⟶ T
15. (f 1 0) = (f x 0) ∈ T
⊢ 1 = 0 ∈ T

---

Latex:

---

Latex:

1.  f  :  \mcap{}A:Type.  (A  {}\mrightarrow{}  A  {}\mrightarrow{}  A)
2.  \mforall{}x,y:Base.    (\mdownarrow{}((f  x  y)  =  x)  \mvee{}  ((f  x  y)  =  y))
3.  \mforall{}z:Base.  ((f  z  z)  =  z)
4.  ((f  0  1)  =  0)  \mvee{}  ((f  0  1)  =  1)
5.  0  =  0
6.  \mforall{}x,y:\mBbbZ{}.    ((f  x  y)  =  x)
7.  (f  1  0)  =  1
8.  \mforall{}y:Base.  ((f  1  y)  =  1)
9.  x  :  Base
10.  (f  x  0)  =  0
11.  T  :  Type
12.  x  =  1
13.  0  =  0
14.  (1  =  0)  {}\mRightarrow{}  (x  =  0)
15.  f  \mmember{}  T  {}\mrightarrow{}  T  {}\mrightarrow{}  T
16.  (f  1  0)  =  (f  x  0)
\mvdash{}  (f  x  0)  =  x


By

---

Latex:
(D  -3  THENM  (HypSubst'  (-1)  0  THEN  Auto))

---

Home Index