---

Step * 3 of Lemma primed-class-opt-single-val0


1. Info : Type
2. B : Type
3. es : EO+(Info)
4. X : EClass(B)
5. init : Id ─→ bag(B)
6. e : E@i
7. v1 : B@i
8. v2 : B@i
9. single-valued-bag(init loc(e);B)@i
10. single-valued-classrel(es;X;B)@i
11. ∀e':E. ((e' <loc e) ⇒ (∀w:B. (¬w ∈ X(e'))))
12. v1 ↓∈ init loc(e)
13. e' : E
14. es-p-local-pred(es;λe'.(↓∃w:B. w ∈ X(e'))) e e'
15. v2 ∈ X(e')
⊢ v1 = v2 ∈ B
BY
{ ((Assert ⌈False⌉⋅ THEN Auto)
   THEN RepUR ``es-p-local-pred`` (-2)
   THEN SquashExRepD
   THEN InstHyp [⌈e'⌉;⌈v2⌉] (-8)⋅
   THEN Auto) }

---

Latex:

---

Latex:

1.  Info  :  Type
2.  B  :  Type
3.  es  :  EO+(Info)
4.  X  :  EClass(B)
5.  init  :  Id  {}\mrightarrow{}  bag(B)
6.  e  :  E@i
7.  v1  :  B@i
8.  v2  :  B@i
9.  single-valued-bag(init  loc(e);B)@i
10.  single-valued-classrel(es;X;B)@i
11.  \mforall{}e':E.  ((e'  <loc  e)  {}\mRightarrow{}  (\mforall{}w:B.  (\mneg{}w  \mmember{}  X(e'))))
12.  v1  \mdownarrow{}\mmember{}  init  loc(e)
13.  e'  :  E
14.  es-p-local-pred(es;\mlambda{}e'.(\mdownarrow{}\mexists{}w:B.  w  \mmember{}  X(e')))  e  e'
15.  v2  \mmember{}  X(e')
\mvdash{}  v1  =  v2


By

---

Latex:
((Assert  \mkleeneopen{}False\mkleeneclose{}\mcdot{}  THEN  Auto)
  THEN  RepUR  ``es-p-local-pred``  (-2)
  THEN  SquashExRepD
  THEN  InstHyp  [\mkleeneopen{}e'\mkleeneclose{};\mkleeneopen{}v2\mkleeneclose{}]  (-8)\mcdot{}
  THEN  Auto)

---

Home Index