---

Step * of Lemma primed-class-opt_functionality

∀[Info,B:Type]. ∀[init:Id ─→ bag(B)]. ∀[es:EO+(Info)]. ∀[e:E]. ∀[X,Y:EClass(B)].
  Prior(X)?init(e) = Prior(Y)?init(e) ∈ bag(B) supposing ∀e1:E. ((e1 < e) ⇒ (X(e1) = Y(e1) ∈ bag(B)))
BY
{ (Auto
   THEN MoveToConcl (-1)
   THEN MoveToConcl (-3)
   THEN Unfold `class-ap` 0
   THEN CausalInd'
   THEN Auto
   THEN (RWO "primed-class-opt-cases" 0 THENA Auto)
   THEN OldAutoSplit) }

---

Latex:

---

Latex:
\mforall{}[Info,B:Type].  \mforall{}[init:Id  {}\mrightarrow{}  bag(B)].  \mforall{}[es:EO+(Info)].  \mforall{}[e:E].  \mforall{}[X,Y:EClass(B)].
    Prior(X)?init(e)  =  Prior(Y)?init(e)  supposing  \mforall{}e1:E.  ((e1  <  e)  {}\mRightarrow{}  (X(e1)  =  Y(e1)))


By

---

Latex:
(Auto
  THEN  MoveToConcl  (-1)
  THEN  MoveToConcl  (-3)
  THEN  Unfold  `class-ap`  0
  THEN  CausalInd'
  THEN  Auto
  THEN  (RWO  "primed-class-opt-cases"  0  THENA  Auto)
  THEN  OldAutoSplit)

---

Home Index