---

Step * of Lemma fpf-rename-dom2

∀[A,C:Type]. ∀[eqa:EqDecider(A)]. ∀[eqc:EqDecider(C)]. ∀[eqc':Top]. ∀[r:A ─→ C]. ∀[f:a:A fp-> Top]. ∀[a:A].
  {↑r a ∈ dom(rename(r;f)) supposing ↑a ∈ dom(f)}
BY
{ (Unfold `guard` 0
   THEN BasicUniformUnivCD Auto
   THEN (UnhideUsingConclWitness THENA Try (Complete (Auto)))
   THEN (Unfolds ``fpf-rename fpf-dom`` 0
         THEN DVar `f'
         THEN Reduce 0
         THEN Auto
         THEN Unfolds ``fpf-rename fpf-dom`` (-1)
         THEN Reduce (-1))⋅) }

1
1. A : Type
2. C : Type
3. eqa : EqDecider(A)
4. eqc : EqDecider(C)
5. eqc' : Top
6. r : A ─→ C
7. d : A List
8. f1 : a:{a:A| (a ∈ d)}  ─→ Top
9. a : A
10. ↑a ∈b d)
⊢ (r a ∈ map(r;d))

---

Latex:


\mforall{}[A,C:Type].  \mforall{}[eqa:EqDecider(A)].  \mforall{}[eqc:EqDecider(C)].  \mforall{}[eqc':Top].  \mforall{}[r:A  {}\mrightarrow{}  C].  \mforall{}[f:a:A  fp->  Top].
\mforall{}[a:A].
    \{\muparrow{}r  a  \mmember{}  dom(rename(r;f))  supposing  \muparrow{}a  \mmember{}  dom(f)\}


By

(Unfold  `guard`  0
  THEN  BasicUniformUnivCD  Auto
  THEN  (UnhideUsingConclWitness  THENA  Try  (Complete  (Auto)))
  THEN  (Unfolds  ``fpf-rename  fpf-dom``  0
              THEN  DVar  `f'
              THEN  Reduce  0
              THEN  Auto
              THEN  Unfolds  ``fpf-rename  fpf-dom``  (-1)
              THEN  Reduce  (-1))\mcdot{})

---

Home Index