---

Step * of Lemma fpf-compose_wf

∀[A:Type]. ∀[B,C:A ─→ Type]. ∀[f:a:A fp-> B[a]]. ∀[g:∩a:A. (B[a] ─→ C[a])].  (g o f ∈ a:A fp-> C[a])
BY
{ (Auto THEN Unfolds ``fpf-compose fpf`` 0 THEN DVar `f' THEN All Reduce THEN Auto) }

1
1. A : Type
2. B : A ─→ Type
3. C : A ─→ Type
4. d : A List
5. f1 : a:{a:A| (a ∈ d)}  ─→ B[a]
6. g : ∩a:A. (B[a] ─→ C[a])
⊢ g o f1 ∈ a:{a:A| (a ∈ d)}  ─→ C[a]

---

Latex:


\mforall{}[A:Type].  \mforall{}[B,C:A  {}\mrightarrow{}  Type].  \mforall{}[f:a:A  fp->  B[a]].  \mforall{}[g:\mcap{}a:A.  (B[a]  {}\mrightarrow{}  C[a])].    (g  o  f  \mmember{}  a:A  fp->  C[a])


By

(Auto  THEN  Unfolds  ``fpf-compose  fpf``  0  THEN  DVar  `f'  THEN  All  Reduce  THEN  Auto)

---

Home Index