---

Step * of Lemma pair-prior-val

∀[Info:Type]. ∀[es:EO+(Info)]. ∀[A,B:Type]. ∀[X:EClass(A)]. ∀[Y:EClass(B)]. ∀[e:E].  X;Y(e) ~ <(X)'(e), Y(e)> supposing \000C↑e ∈b X;Y
BY
{ (Auto
   THEN (RWO "is-pair-prior" (-1) THENA Auto)
   THEN Unfold `es-interface-pair-prior` 0
   THEN RW (AddrC [1] UnfoldTopAbC) 0
   THEN Reduce 0
   THEN RepeatFor 2 (OldAutoSplit)) }

---

Latex:

---

Latex:
\mforall{}[Info:Type].  \mforall{}[es:EO+(Info)].  \mforall{}[A,B:Type].  \mforall{}[X:EClass(A)].  \mforall{}[Y:EClass(B)].  \mforall{}[e:E].
    X;Y(e)  \msim{}  <(X)'(e),  Y(e)>  supposing  \muparrow{}e  \mmember{}\msubb{}  X;Y


By

---

Latex:
(Auto
  THEN  (RWO  "is-pair-prior"  (-1)  THENA  Auto)
  THEN  Unfold  `es-interface-pair-prior`  0
  THEN  RW  (AddrC  [1]  UnfoldTopAbC)  0
  THEN  Reduce  0
  THEN  RepeatFor  2  (OldAutoSplit))

---

Home Index