---

Step * of Lemma member-fpf-domain-variant

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

---

Latex:

---

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


By

---

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

---

Home Index