---

Step * of Lemma fpf-rename-dom

∀[A,C:Type]. ∀[B:A ─→ Type].
  ∀eqa:EqDecider(A). ∀eqc:EqDecider(C). ∀r:A ─→ C. ∀f:a:A fp-> B[a]. ∀c:C.
    (↑c ∈ dom(rename(r;f)) ⇐⇒ ∃a:A. ((↑a ∈ dom(f)) c∧ (c = (r a) ∈ C)))
BY
{ ((((UnivCD THENA Auto)
     THEN Unfolds ``fpf-rename fpf-dom`` 0
     THEN DVar `f'
     THEN Reduce 0
     THEN RWO "assert-deq-member" 0)
    THENA Auto
    )
   THEN RWO "member_map" 0
   THEN Auto) }

---

Latex:


\mforall{}[A,C:Type].  \mforall{}[B:A  {}\mrightarrow{}  Type].
    \mforall{}eqa:EqDecider(A).  \mforall{}eqc:EqDecider(C).  \mforall{}r:A  {}\mrightarrow{}  C.  \mforall{}f:a:A  fp->  B[a].  \mforall{}c:C.
        (\muparrow{}c  \mmember{}  dom(rename(r;f))  \mLeftarrow{}{}\mRightarrow{}  \mexists{}a:A.  ((\muparrow{}a  \mmember{}  dom(f))  c\mwedge{}  (c  =  (r  a))))


By

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

---

Home Index