---

Step * of Lemma hdf-bind-compose1-left

∀[A,B,C,U:Type]. ∀[f:B ─→ C]. ∀[X:hdataflow(A;B)]. ∀[Y:C ─→ hdataflow(A;U)].
  (f o X >>= Y = X >>= Y o f ∈ hdataflow(A;U)) supposing (valueall-type(C) and valueall-type(U))
BY
{ (Auto THEN (RWO "hdf-bind-as-gen" 0 THENA Auto) THEN (RWO "hdf-bind-gen-compose1-left" 0 THENA Auto)) }

---

Latex:


\mforall{}[A,B,C,U:Type].  \mforall{}[f:B  {}\mrightarrow{}  C].  \mforall{}[X:hdataflow(A;B)].  \mforall{}[Y:C  {}\mrightarrow{}  hdataflow(A;U)].
    (f  o  X  >>=  Y  =  X  >>=  Y  o  f)  supposing  (valueall-type(C)  and  valueall-type(U))


By

(Auto
  THEN  (RWO  "hdf-bind-as-gen"  0  THENA  Auto)
  THEN  (RWO  "hdf-bind-gen-compose1-left"  0  THENA  Auto))

---

Home Index