---

Step * of Lemma member-fpf-domain

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

---

Latex:


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


By

((UnivCD  THENA  Auto)
  THEN  DVar  `f'
  THEN  Unfolds  ``fpf-dom  fpf-domain``  0
  THEN  Reduce  0
  THEN  RWO  "assert-deq-member"  0
  THEN  Auto)

---

Home Index