---

Step * of Lemma dataflow-equiv_transitivity

∀[A,B:Type]. ∀[f,g,h:dataflow(A;B)].  (f ≡ h) supposing (f ≡ g and g ≡ h)
BY
{ ((Auto THEN All (Unfold `dataflow-equiv`)) THEN RepeatFor 2 (ParallelLast)) }

---

Latex:

---

Latex:
\mforall{}[A,B:Type].  \mforall{}[f,g,h:dataflow(A;B)].    (f  \mequiv{}  h)  supposing  (f  \mequiv{}  g  and  g  \mequiv{}  h)


By

---

Latex:
((Auto  THEN  All  (Unfold  `dataflow-equiv`))  THEN  RepeatFor  2  (ParallelLast))

---

Home Index