---

Step * of Lemma hdf-base-ap-fst

∀[A,B:Type]. ∀[F:A ⟶ bag(B)]. ∀[a:A].  ((fst(hdf-base(m.F[m])(a))) = hdf-base(m.F[m]) ∈ hdataflow(A;B))
BY
{ Auto }

---

Latex:

---

Latex:
\mforall{}[A,B:Type].  \mforall{}[F:A  {}\mrightarrow{}  bag(B)].  \mforall{}[a:A].    ((fst(hdf-base(m.F[m])(a)))  =  hdf-base(m.F[m]))


By

---

Latex:
Auto

---

Home Index