---

Step * of Lemma fpf-ap_wf

∀[A:Type]. ∀[B:A ─→ Type]. ∀[f:a:A fp-> B[a]]. ∀[eq:EqDecider(A)]. ∀[x:A].  f(x) ∈ B[x] supposing ↑x ∈ dom(f)
BY
{ (Unfolds ``fpf fpf-dom fpf-ap`` 0 THEN Auto) }

1
1. A : Type
2. B : A ─→ Type
3. f : d:A List × (a:{a:A| (a ∈ d)}  ─→ B[a])
4. eq : EqDecider(A)
5. x : A
6. ↑x ∈b fst(f))
⊢ x ∈ {a:A| (a ∈ fst(f))} 

---

Latex:


\mforall{}[A:Type].  \mforall{}[B:A  {}\mrightarrow{}  Type].  \mforall{}[f:a:A  fp->  B[a]].  \mforall{}[eq:EqDecider(A)].  \mforall{}[x:A].
    f(x)  \mmember{}  B[x]  supposing  \muparrow{}x  \mmember{}  dom(f)


By

(Unfolds  ``fpf  fpf-dom  fpf-ap``  0  THEN  Auto)

---

Home Index