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