---

Step * of Lemma hdf-parallel-bag_wf

∀[A,B:Type]. ∀[Xs:bag(hdataflow(A;B))].  hdf-parallel-bag(Xs) ∈ hdataflow(A;B) supposing valueall-type(B)
BY
{ ProveWfLemmaAux (Try (Complete Auto)) }

---

Latex:

---

Latex:
\mforall{}[A,B:Type].  \mforall{}[Xs:bag(hdataflow(A;B))].
    hdf-parallel-bag(Xs)  \mmember{}  hdataflow(A;B)  supposing  valueall-type(B)


By

---

Latex:
ProveWfLemmaAux  (Try  (Complete  Auto))

---

Home Index