---

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


1. f : ⋂A:Type. (A ⟶ A ⟶ A)
2. ∀x,y:Base.  (↓((f x y) = x ∈ Base) ∨ ((f x y) = y ∈ Base))
3. f ∈ ℤ ⟶ ℤ ⟶ ℤ
4. (f 0 1) = 0 ∈ ℤ
5. x : ℤ
6. y : ℤ
7. (f x y) = y ∈ Base
8. ¬(x = y ∈ ℤ)
9. n : ℤ
10. m : ℤ
11. ¬(n = m ∈ ℤ)
12. (f n m) = n ∈ ℤ
13. ¬(x = m ∈ ℤ)
14. ¬(y = n ∈ ℤ)
15. T : Type
16. x = n ∈ T
17. y = m ∈ T
18. ¬(x = y ∈ T)
19. g : T ⟶ T ⟶ T
20. f = g ∈ (T ⟶ T ⟶ T)
⊢ ((g x y) = y ∈ T) ⇒ ((g n m) = n ∈ T) ⇒ False
BY
{ ((RevHypSubst (-5) 0 THENA Auto) THEN RevHypSubst (-4) 0 THEN Auto) }

---

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.  f  \mmember{}  \mBbbZ{}  {}\mrightarrow{}  \mBbbZ{}  {}\mrightarrow{}  \mBbbZ{}
4.  (f  0  1)  =  0
5.  x  :  \mBbbZ{}
6.  y  :  \mBbbZ{}
7.  (f  x  y)  =  y
8.  \mneg{}(x  =  y)
9.  n  :  \mBbbZ{}
10.  m  :  \mBbbZ{}
11.  \mneg{}(n  =  m)
12.  (f  n  m)  =  n
13.  \mneg{}(x  =  m)
14.  \mneg{}(y  =  n)
15.  T  :  Type
16.  x  =  n
17.  y  =  m
18.  \mneg{}(x  =  y)
19.  g  :  T  {}\mrightarrow{}  T  {}\mrightarrow{}  T
20.  f  =  g
\mvdash{}  ((g  x  y)  =  y)  {}\mRightarrow{}  ((g  n  m)  =  n)  {}\mRightarrow{}  False


By

---

Latex:
((RevHypSubst  (-5)  0  THENA  Auto)  THEN  RevHypSubst  (-4)  0  THEN  Auto)

---

Home Index