---

Step * of Lemma fpf-const-dom

∀[A:Type]. ∀eq:EqDecider(A). ∀L:A List. ∀v:Top. ∀x:A.  (↑x ∈ dom(L |-fpf-> v) ⇐⇒ (x ∈ L))
BY
{ (Unfolds ``fpf-dom fpf-const`` 0 THEN Reduce 0 THEN Auto THEN All (RWO "assert-deq-member")⋅ THEN Auto) }

---

Latex:


\mforall{}[A:Type].  \mforall{}eq:EqDecider(A).  \mforall{}L:A  List.  \mforall{}v:Top.  \mforall{}x:A.    (\muparrow{}x  \mmember{}  dom(L  |-fpf->  v)  \mLeftarrow{}{}\mRightarrow{}  (x  \mmember{}  L))


By

(Unfolds  ``fpf-dom  fpf-const``  0
  THEN  Reduce  0
  THEN  Auto
  THEN  All  (RWO  "assert-deq-member")\mcdot{}
  THEN  Auto)

---

Home Index