Step * 1 of Lemma eq_int_eq_false_elim


1. : ℤ
2. : ℤ
3. (i =z j) ff
⊢ i ≠ j
BY
(Decide ⌜j ∈ ℤ⌝ THEN Auto) }

1
1. : ℤ
2. : ℤ
3. (i =z j) ff
4. j ∈ ℤ
⊢ i ≠ j


Latex:


Latex:

1.  i  :  \mBbbZ{}
2.  j  :  \mBbbZ{}
3.  (i  =\msubz{}  j)  =  ff
\mvdash{}  i  \mneq{}  j


By


Latex:
(Decide  \mkleeneopen{}i  =  j\mkleeneclose{}  THEN  Auto)




Home Index