---

Step * of Lemma fpf-rename-ap2

∀[A,C:Type]. ∀[B:A ─→ Type]. ∀[eqa:EqDecider(A)]. ∀[eqc,eqc':EqDecider(C)]. ∀[r:A ─→ C]. ∀[f:a:A fp-> B[a]]. ∀[a:A].
  (rename(r;f)(r a) = f(a) ∈ B[a]) supposing ((↑a ∈ dom(f)) and Inj(A;C;r))
BY
{ (((UnivCD THENA Auto)
    THEN Unfolds ``fpf-rename fpf-ap`` 0
    THEN DVar `f'
    THEN Reduce 0
    THEN (InstLemma `hd-filter` [A; λ2y.eqc (r y) (r a); d])⋅)
   THENA Auto
   ) }

1
.....antecedent..... 
1. A : Type
2. C : Type
3. B : A ─→ Type
4. eqa : EqDecider(A)
5. eqc : EqDecider(C)
6. eqc' : EqDecider(C)
7. r : A ─→ C
8. d : A List
9. f1 : a:{a:A| (a ∈ d)}  ─→ B[a]
10. a : A
11. Inj(A;C;r)
12. ↑a ∈ dom(<d, f1>)
⊢ ∃a@0:A. ((a@0 ∈ d) ∧ (↑(eqc (r a@0) (r a))))

2
1. A : Type
2. C : Type
3. B : A ─→ Type
4. eqa : EqDecider(A)
5. eqc : EqDecider(C)
6. eqc' : EqDecider(C)
7. r : A ─→ C
8. d : A List
9. f1 : a:{a:A| (a ∈ d)}  ─→ B[a]
10. a : A
11. Inj(A;C;r)
12. ↑a ∈ dom(<d, f1>)
13. (hd(filter(λa@0.(eqc (r a@0) (r a));d)) ∈ A)
c∧ ((hd(filter(λa@0.(eqc (r a@0) (r a));d)) ∈ d) ∧ (↑(eqc (r hd(filter(λa@0.(eqc (r a@0) (r a));d))) (r a))))
⊢ (f1 hd(filter(λy.(eqc (r y) (r a));d))) = (f1 a) ∈ B[a]

---

Latex:


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


By

(((UnivCD  THENA  Auto)
    THEN  Unfolds  ``fpf-rename  fpf-ap``  0
    THEN  DVar  `f'
    THEN  Reduce  0
    THEN  (InstLemma  `hd-filter`  [A;  \mlambda{}\msubtwo{}y.eqc  (r  y)  (r  a);  d])\mcdot{})
  THENA  Auto
  )

---

Home Index