---

Step * of Lemma dataflow-equiv_inversion

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

---

Latex:

---

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


By

---

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

---

Home Index