---

Step * of Lemma local-class-predicate-property

∀[Info,A:Type]. ∀[X:EClass(A)]. ∀[F1,F2:Id ─→ hdataflow(Info;A)].
  (local-class-predicate{i:l}(F2;Info;A;X)) supposing 
     (local-class-predicate{i:l}(F1;Info;A;X) and 
     (∀i:Id. (F1[i] = F2[i] ∈ hdataflow(Info;A))))
BY
{ (Auto
   THEN All (Unfold `local-class-predicate`)
   THEN Auto
   THEN (InstHyp [⌈loc(e)⌉] (-4)⋅ THENA Auto)
   THEN (InstHyp [⌈es⌉;⌈e⌉] (-4)⋅ THENA Auto)
   THEN RepUR ``so_apply`` (-2)
   THEN RevHypSubst' (-2) 0
   THEN Auto) }

---

Latex:


\mforall{}[Info,A:Type].  \mforall{}[X:EClass(A)].  \mforall{}[F1,F2:Id  {}\mrightarrow{}  hdataflow(Info;A)].
    (local-class-predicate\{i:l\}(F2;Info;A;X))  supposing 
          (local-class-predicate\{i:l\}(F1;Info;A;X)  and 
          (\mforall{}i:Id.  (F1[i]  =  F2[i])))


By

(Auto
  THEN  All  (Unfold  `local-class-predicate`)
  THEN  Auto
  THEN  (InstHyp  [\mkleeneopen{}loc(e)\mkleeneclose{}]  (-4)\mcdot{}  THENA  Auto)
  THEN  (InstHyp  [\mkleeneopen{}es\mkleeneclose{};\mkleeneopen{}e\mkleeneclose{}]  (-4)\mcdot{}  THENA  Auto)
  THEN  RepUR  ``so\_apply``  (-2)
  THEN  RevHypSubst'  (-2)  0
  THEN  Auto)

---

Home Index