---

Step * of Lemma int-decr-map-empty-prop

∀[Value:Type]. ∀[k:ℤ].  (¬↑int-decr-map-inDom(k;int-decr-map-empty()))
BY
{ (Auto THEN RepUR ``int-decr-map-inDom int-decr-map-empty int-decr-map-find`` 0 THEN Auto) }

---

Latex:


\mforall{}[Value:Type].  \mforall{}[k:\mBbbZ{}].    (\mneg{}\muparrow{}int-decr-map-inDom(k;int-decr-map-empty()))


By

(Auto  THEN  RepUR  ``int-decr-map-inDom  int-decr-map-empty  int-decr-map-find``  0  THEN  Auto)

---

Home Index