---

Step * 1 1 1 1 1 1 of Lemma assert_of_eq_int


1. x : ℤ
2. y : ℤ
3. ↑if x=y then tt else ff
4. (x + (-x)) = 0 ∈ ℤ
5. x < x
6. 0 < 0
⊢ False
BY
{ Auto }

---

Latex:

---

Latex:

1.  x  :  \mBbbZ{}
2.  y  :  \mBbbZ{}
3.  \muparrow{}if  x=y  then  tt  else  ff
4.  (x  +  (-x))  =  0
5.  x  <  x
6.  0  <  0
\mvdash{}  False


By

---

Latex:
Auto

---

Home Index