---

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
{ ((Intros THEN Unhide)
   THEN DVar `f'
   THEN Unfolds ``fpf-rename fpf`` 0
   THEN Reduce 0
   THEN (Assert ⌜∀x:{c:C| (c ∈ map(r;d))} . (f1 hd(filter(λy.(eq (r y) x);d)) ∈ D[x])⌝⋅ THENM Auto)
   THEN (D 0 THENA Auto)) }

1
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))} 
⊢ f1 hd(filter(λy.(eq (r y) x);d)) ∈ D[x]

---

Latex:

---

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

---

Latex:
((Intros  THEN  Unhide)
  THEN  DVar  `f'
  THEN  Unfolds  ``fpf-rename  fpf``  0
  THEN  Reduce  0
  THEN  (Assert  \mkleeneopen{}\mforall{}x:\{c:C|  (c  \mmember{}  map(r;d))\}  .  (f1  hd(filter(\mlambda{}y.(eq  (r  y)  x);d))  \mmember{}  D[x])\mkleeneclose{}\mcdot{}  THENM  Auto)
  THEN  (D  0  THENA  Auto))

---

Home Index