---

Step * of Lemma hdataflow_subtype

∀[A1,B1,A2,B2:Type].  (hdataflow(A1;B1) ⊆r hdataflow(A2;B2)) supposing ((B1 ⊆r B2) and (A2 ⊆r A1))
BY
{ (Auto THEN Unfold `hdataflow` 0 THEN Try (BLemma `corec-subtype-corec2`) THEN Auto) }

---

Latex:


\mforall{}[A1,B1,A2,B2:Type].    (hdataflow(A1;B1)  \msubseteq{}r  hdataflow(A2;B2))  supposing  ((B1  \msubseteq{}r  B2)  and  (A2  \msubseteq{}r  A1))


By

(Auto  THEN  Unfold  `hdataflow`  0  THEN  Try  (BLemma  `corec-subtype-corec2`)  THEN  Auto)

---

Home Index