---

Step * of Lemma fpf-type

∀[A:Type]. ∀[B:A ─→ Type]. ∀[f:a:A fp-> B[a]].  (f ∈ a:{a:A| (a ∈ fpf-domain(f))}  fp-> B[a])
BY
{ (Auto THEN All (Unfold `fpf`)) }

1
1. A : Type
2. B : A ─→ Type
3. f : d:A List × (a:{a:A| (a ∈ d)}  ─→ B[a])
⊢ f ∈ d:{a:A| (a ∈ fpf-domain(f))}  List × (a:{a:{a:A| (a ∈ fpf-domain(f))} | (a ∈ d)}  ─→ B[a])

---

Latex:


\mforall{}[A:Type].  \mforall{}[B:A  {}\mrightarrow{}  Type].  \mforall{}[f:a:A  fp->  B[a]].    (f  \mmember{}  a:\{a:A|  (a  \mmember{}  fpf-domain(f))\}    fp->  B[a])


By

(Auto  THEN  All  (Unfold  `fpf`))

---

Home Index