---

Step * of Lemma local-class-predicate-property2

∀[Info,A:Type]. ∀[X1,X2:EClass(A)]. ∀[F:Id ─→ hdataflow(Info;A)].
  (local-class-predicate{i:l}(F;Info;A;X1)) supposing 
     (local-class-predicate{i:l}(F;Info;A;X2) and 
     (∀es:EO+(Info). ∀e:E.  (X1(e) = X2(e) ∈ bag(A))))
BY
{ (Auto THEN All (Unfold `local-class-predicate`) THEN Auto THEN RWO "-4" 0 THEN Auto) }

---

Latex:


\mforall{}[Info,A:Type].  \mforall{}[X1,X2:EClass(A)].  \mforall{}[F:Id  {}\mrightarrow{}  hdataflow(Info;A)].
    (local-class-predicate\{i:l\}(F;Info;A;X1))  supposing 
          (local-class-predicate\{i:l\}(F;Info;A;X2)  and 
          (\mforall{}es:EO+(Info).  \mforall{}e:E.    (X1(e)  =  X2(e))))


By

(Auto  THEN  All  (Unfold  `local-class-predicate`)  THEN  Auto  THEN  RWO  "-4"  0  THEN  Auto)

---

Home Index