---

Step * 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. x + (-x) < x + (-x)
⊢ False
BY
{ HypSubst' (-3) (-1) }

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

---

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.  x  +  (-x)  <  x  +  (-x)
\mvdash{}  False


By

---

Latex:
HypSubst'  (-3)  (-1)

---

Home Index