---

Step * of Lemma member-fpf-dom

∀[A:Type]. ∀eq:EqDecider(A). ∀f:a:A fp-> Top. ∀x:A.  (↑x ∈ dom(f) ⇐⇒ (x ∈ fst(f)))
BY
{ (Unfolds ``fpf fpf-dom`` 0 THEN RWO "assert-deq-member" 0 THEN Auto) }

---

Latex:


\mforall{}[A:Type].  \mforall{}eq:EqDecider(A).  \mforall{}f:a:A  fp->  Top.  \mforall{}x:A.    (\muparrow{}x  \mmember{}  dom(f)  \mLeftarrow{}{}\mRightarrow{}  (x  \mmember{}  fst(f)))


By

(Unfolds  ``fpf  fpf-dom``  0  THEN  RWO  "assert-deq-member"  0  THEN  Auto)

---

Home Index