---

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

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:

---

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

---

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

---

Home Index