---

Step * of Lemma primed-class-opt_eq_class-opt-class-primed

∀[Info,T:Type]. ∀[init:Id ⟶ bag(T)]. ∀[X:EClass(T)].  (Prior(X)?init = Prior(X)?λl.init l| | ∈ EClass(T))
BY
{ ((UnivCD THENA Auto)
   THEN RepUR ``primed-class-opt class-opt-class primed-class simple-loc-comb0 simple-loc-comb eclass`` 0
   THEN RepeatFor 2 ((MemCD THENA Auto))
   THEN (SplitOnConclITE  THENA Auto)
   THEN Reduce 0
   THEN Auto
   THEN GenConclAtAddr [2;1]
   THEN D (-2)
   THEN Reduce 0
   THEN Auto
   THEN Try (Complete (((HypSubst' (-1) (-3) THENA Auto) THEN Reduce (-1) THEN D (-1) THEN Auto)))
   THEN D (-2)
   THEN RepD
   THEN (HypSubst' (-1) (-6) THENA Auto)
   THEN Reduce (-1)
   THEN Reduce (-4)
   THEN (HypSubst' (-1) (-4) THENA Auto)
   THEN Reduce (-4)
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[Info,T:Type].  \mforall{}[init:Id  {}\mrightarrow{}  bag(T)].  \mforall{}[X:EClass(T)].    (Prior(X)?init  =  Prior(X)?\mlambda{}l.init  l|  |)


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  ...
  THEN  RepeatFor  2  ((MemCD  THENA  Auto))
  THEN  (SplitOnConclITE    THENA  Auto)
  THEN  Reduce  0
  THEN  Auto
  THEN  GenConclAtAddr  [2;1]
  THEN  D  (-2)
  THEN  Reduce  0
  THEN  Auto
  THEN  Try  (Complete  (((HypSubst'  (-1)  (-3)  THENA  Auto)  THEN  Reduce  (-1)  THEN  D  (-1)  THEN  Auto)))
  THEN  D  (-2)
  THEN  RepD
  THEN  (HypSubst'  (-1)  (-6)  THENA  Auto)
  THEN  Reduce  (-1)
  THEN  Reduce  (-4)
  THEN  (HypSubst'  (-1)  (-4)  THENA  Auto)
  THEN  Reduce  (-4)
  THEN  Auto)

---

Home Index