---

Step * 1 1 2 of Lemma assert_of_eq_int


1. x : ℤ
2. y : ℤ
3. ↑if x=y then tt else ff
4. ¬x < x
⊢ x = y ∈ ℤ
BY
{ ((InstLemma `less-trichotomy` [⌜x⌝;⌜y⌝]⋅ THENA Auto)
   THEN SplitOrHyps
   THEN Try (Trivial)
   THEN (Subst' if x=y then tt else ff ~ ff -3 THENM (Reduce (-3) THEN FalseHD (-3)))
   THEN Refine_int_eqReduceFalseSq
   THEN Auto) }

---

Latex:

---

Latex:

1.  x  :  \mBbbZ{}
2.  y  :  \mBbbZ{}
3.  \muparrow{}if  x=y  then  tt  else  ff
4.  \mneg{}x  <  x
\mvdash{}  x  =  y


By

---

Latex:
((InstLemma  `less-trichotomy`  [\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  SplitOrHyps
  THEN  Try  (Trivial)
  THEN  (Subst'  if  x=y  then  tt  else  ff  \msim{}  ff  -3  THENM  (Reduce  (-3)  THEN  FalseHD  (-3)))
  THEN  Refine\_int\_eqReduceFalseSq
  THEN  Auto)

---

Home Index