---

Step * of Lemma fpf-inv-rename_wf

∀[A,C:Type]. ∀[B:A ─→ Type]. ∀[D:C ─→ Type]. ∀[rinv:C ─→ (A?)]. ∀[r:A ─→ C]. ∀[f:c:C fp-> D[c]].
  (fpf-inv-rename(r;rinv;f) ∈ a:A fp-> B[a]) supposing ((∀a:A. (D[r a] = B[a] ∈ Type)) and inv-rel(A;C;r;rinv))
BY
{ ((Auto THEN Unfolds ``fpf-inv-rename fpf`` 0 THEN DVar `f' THEN Reduce 0 THEN MemCD) THENA Auto) }

1
.....subterm..... T:t
1:n
1. A : Type
2. C : Type
3. B : A ─→ Type
4. D : C ─→ Type
5. rinv : C ─→ (A?)
6. r : A ─→ C
7. d : C List
8. f1 : c:{c:C| (c ∈ d)}  ─→ D[c]
9. inv-rel(A;C;r;rinv)
10. ∀a:A. (D[r a] = B[a] ∈ Type)
⊢ mapfilter(λx.outl(rinv x);λx.isl(rinv x);d) ∈ A List

2
.....subterm..... T:t
2:n
1. A : Type
2. C : Type
3. B : A ─→ Type
4. D : C ─→ Type
5. rinv : C ─→ (A?)
6. r : A ─→ C
7. d : C List
8. f1 : c:{c:C| (c ∈ d)}  ─→ D[c]
9. inv-rel(A;C;r;rinv)
10. ∀a:A. (D[r a] = B[a] ∈ Type)
⊢ f1 o r ∈ a:{a:A| (a ∈ mapfilter(λx.outl(rinv x);λx.isl(rinv x);d))}  ─→ B[a]

---

Latex:


\mforall{}[A,C:Type].  \mforall{}[B:A  {}\mrightarrow{}  Type].  \mforall{}[D:C  {}\mrightarrow{}  Type].  \mforall{}[rinv:C  {}\mrightarrow{}  (A?)].  \mforall{}[r:A  {}\mrightarrow{}  C].  \mforall{}[f:c:C  fp->  D[c]].
    (fpf-inv-rename(r;rinv;f)  \mmember{}  a:A  fp->  B[a])  supposing 
          ((\mforall{}a:A.  (D[r  a]  =  B[a]))  and 
          inv-rel(A;C;r;rinv))


By

((Auto  THEN  Unfolds  ``fpf-inv-rename  fpf``  0  THEN  DVar  `f'  THEN  Reduce  0  THEN  MemCD)  THENA  Auto)

---

Home Index