---

Step * 1 of Lemma fpf-type


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])
BY
{ (D -1 THEN Unfold `fpf-domain` 0 THEN Reduce 0) }

1
1. A : Type
2. B : A ─→ Type
3. d : A List
4. f1 : a:{a:A| (a ∈ d)}  ─→ B[a]
⊢ <d, f1> ∈ d@0:{a:A| (a ∈ d)}  List × (a:{a:{a:A| (a ∈ d)} | (a ∈ d@0)}  ─→ B[a])

---

Latex:



1.  A  :  Type
2.  B  :  A  {}\mrightarrow{}  Type
3.  f  :  d:A  List  \mtimes{}  (a:\{a:A|  (a  \mmember{}  d)\}    {}\mrightarrow{}  B[a])
\mvdash{}  f  \mmember{}  d:\{a:A|  (a  \mmember{}  fpf-domain(f))\}    List  \mtimes{}  (a:\{a:\{a:A|  (a  \mmember{}  fpf-domain(f))\}  |  (a  \mmember{}  d)\}    {}\mrightarrow{}  B[a])


By

(D  -1  THEN  Unfold  `fpf-domain`  0  THEN  Reduce  0)

---

Home Index