---

Step * of Lemma fpf-rename_wf

∀[A,C:Type]. ∀[B:A ─→ Type]. ∀[D:C ─→ Type]. ∀[eq:EqDecider(C)]. ∀[r:A ─→ C]. ∀[f:a:A fp-> B[a]].
  rename(r;f) ∈ c:C fp-> D[c] supposing ∀a:A. (D[r a] = B[a] ∈ Type)
BY
{ (Auto
   THEN DVar `f'
   THEN Unfolds ``fpf-rename fpf`` 0
   THEN Reduce 0
   THEN RepeatFor 2 ((MemCD THEN Try (Complete (Auto))))) }

1
.....subterm..... T:t
1:n
1. A : Type
2. C : Type
3. B : A ─→ Type
4. D : C ─→ Type
5. eq : EqDecider(C)
6. r : A ─→ C
7. d : A List
8. f1 : a:{a:A| (a ∈ d)}  ─→ B[a]
9. ∀a:A. (D[r a] = B[a] ∈ Type)
10. x : {c:C| (c ∈ map(r;d))} @i
⊢ f1 hd(filter(λy.(eq (r y) x);d)) ∈ D[x]

---

Latex:


\mforall{}[A,C:Type].  \mforall{}[B:A  {}\mrightarrow{}  Type].  \mforall{}[D:C  {}\mrightarrow{}  Type].  \mforall{}[eq:EqDecider(C)].  \mforall{}[r:A  {}\mrightarrow{}  C].  \mforall{}[f:a:A  fp->  B[a]].
    rename(r;f)  \mmember{}  c:C  fp->  D[c]  supposing  \mforall{}a:A.  (D[r  a]  =  B[a])


By

(Auto
  THEN  DVar  `f'
  THEN  Unfolds  ``fpf-rename  fpf``  0
  THEN  Reduce  0
  THEN  RepeatFor  2  ((MemCD  THEN  Try  (Complete  (Auto)))))

---

Home Index