---

Step * of Lemma int-decr-map-find-wf

∀[Value:Type]. ∀[k:ℤ]. ∀[m:int-decr-map-type(Value)].  (int-decr-map-find(k;m) ∈ Value?)
BY
{ ((UnivCD THENA Auto) THEN GenConclAtAddr [2] THEN DProdsAndUnions THEN Auto) }

---

Latex:


\mforall{}[Value:Type].  \mforall{}[k:\mBbbZ{}].  \mforall{}[m:int-decr-map-type(Value)].    (int-decr-map-find(k;m)  \mmember{}  Value?)


By

((UnivCD  THENA  Auto)  THEN  GenConclAtAddr  [2]  THEN  DProdsAndUnions  THEN  Auto)

---

Home Index