---

Step * of Lemma int-minus-comparison-inc_wf

∀[T:Type]. ∀[f:T ⟶ ℤ].  (int-minus-comparison-inc(f) ∈ comparison(T))
BY
{ (Auto THEN RepUR ``int-minus-comparison-inc comparison`` 0 THEN MemTypeCD THEN Reduce 0 THEN Auto') }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[f:T  {}\mrightarrow{}  \mBbbZ{}].    (int-minus-comparison-inc(f)  \mmember{}  comparison(T))


By

---

Latex:
(Auto  THEN  RepUR  ``int-minus-comparison-inc  comparison``  0  THEN  MemTypeCD  THEN  Reduce  0  THEN  Auto')

---

Home Index