---

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
{ xxx((((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)xxx }

---

Latex:

---

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

---

Latex:
xxx((((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)xxx

---

Home Index