---

Step * of Lemma int-decr-map-isEmpty-assert

∀[Value:Type]. ∀[m:int-decr-map-type(Value)].
  uiff(↑int-decr-map-isEmpty(m);m = int-decr-map-empty() ∈ int-decr-map-type(Value))
BY
{ (Auto
   THEN Try (((HypSubst (-1) 0 THENA Auto) THEN RW (SymbolicComputeC []) 0 THEN Auto))
   THEN RepUR ``int-decr-map-isEmpty`` (-1)
   THEN AllPushDown
   THEN EqTypeCD
   THEN Auto
   THEN Try ((Unfold `int-decr-map-empty` 0 THEN Auto))
   THEN D (-2)
   THEN Unhide
   THEN Auto) }

---

Latex:


\mforall{}[Value:Type].  \mforall{}[m:int-decr-map-type(Value)].
    uiff(\muparrow{}int-decr-map-isEmpty(m);m  =  int-decr-map-empty())


By

(Auto
  THEN  Try  (((HypSubst  (-1)  0  THENA  Auto)  THEN  RW  (SymbolicComputeC  [])  0  THEN  Auto))
  THEN  RepUR  ``int-decr-map-isEmpty``  (-1)
  THEN  AllPushDown
  THEN  EqTypeCD
  THEN  Auto
  THEN  Try  ((Unfold  `int-decr-map-empty`  0  THEN  Auto))
  THEN  D  (-2)
  THEN  Unhide
  THEN  Auto)

---

Home Index