---

Step * of Lemma local-class-output-agree2

∀[Info,A:Type]. ∀[X:EClass(A)].
  ∀[eo1,eo2:EO+(Info)]. ∀[e1:E]. ∀[e2:E].
    (X(e1) = X(e2) ∈ bag(A)) supposing (eo-local-agree(Info;eo1;eo2;e1;e2) and (loc(e1) = loc(e2) ∈ Id)) 
  supposing LocalClass(X)
BY
{ (InstLemma `local-class-output-agree` [] THEN Auto) }

---

Latex:


\mforall{}[Info,A:Type].  \mforall{}[X:EClass(A)].
    \mforall{}[eo1,eo2:EO+(Info)].  \mforall{}[e1:E].  \mforall{}[e2:E].
        (X(e1)  =  X(e2))  supposing  (eo-local-agree(Info;eo1;eo2;e1;e2)  and  (loc(e1)  =  loc(e2))) 
    supposing  LocalClass(X)


By

(InstLemma  `local-class-output-agree`  []  THEN  Auto)

---

Home Index