---

Step * of Lemma process-equiv-is-equiv

∀[M:Type ⟶ Type]. EquivRel(Process(T.M[T]);P,Q.P≡Q) supposing Continuous+(T.M[T])
BY
{ (Auto
   THEN RepeatFor 2 ((D 0 THEN Auto))
   THEN All (RepUR ``process-equiv``)
   THEN Auto
   THEN ∀h:hyp. (InstHyp [⌜msgs⌝] h⋅ THEN Auto) ) }

---

Latex:

---

Latex:
\mforall{}[M:Type  {}\mrightarrow{}  Type].  EquivRel(Process(T.M[T]);P,Q.P\mequiv{}Q)  supposing  Continuous+(T.M[T])


By

---

Latex:
(Auto
  THEN  RepeatFor  2  ((D  0  THEN  Auto))
  THEN  All  (RepUR  ``process-equiv``)
  THEN  Auto
  THEN  \mforall{}h:hyp.  (InstHyp  [\mkleeneopen{}msgs\mkleeneclose{}]  h\mcdot{}  THEN  Auto)  )

---

Home Index