---

Step * of Lemma is-pair-prior

∀[Info:Type]. ∀[es:EO+(Info)]. ∀[X,Y:EClass(Top)]. ∀[e:E].  uiff(↑e ∈b X;Y;(↑e ∈b (X)') ∧ (↑e ∈b Y))
BY
{ ((UnivCD THENA Auto)
   THEN Unfold `es-interface-pair-prior` 0
   THEN RW (AddrC [1;1] UnfoldTopAbC) 0
   THEN Reduce 0
   THEN RepeatFor 2 (AutoSplit)) }

---

Latex:

---

Latex:
\mforall{}[Info:Type].  \mforall{}[es:EO+(Info)].  \mforall{}[X,Y:EClass(Top)].  \mforall{}[e:E].    uiff(\muparrow{}e  \mmember{}\msubb{}  X;Y;(\muparrow{}e  \mmember{}\msubb{}  (X)')  \mwedge{}  (\muparrow{}e  \mmember{}\msubb{}  Y))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  Unfold  `es-interface-pair-prior`  0
  THEN  RW  (AddrC  [1;1]  UnfoldTopAbC)  0
  THEN  Reduce  0
  THEN  RepeatFor  2  (AutoSplit))

---

Home Index