---

Step * 3 of Lemma rec-combined-class-opt-1-single-val0


1. Info : Type
2. A : Type
3. B : Type
4. es : EO+(Info)
5. F : A ⟶ B ⟶ B
6. X : EClass(A)
7. init : Id ⟶ bag(B)
8. e : E@i
9. ∀e':E
     ((e' < e)
     ⇒ (∀v1,v2:B.
           (single-valued-bag(init loc(e');B)
           ⇒ single-valued-classrel(es;X;A)
           ⇒ v2 ∈ lifting-2(F)|X,Prior(self)?init|(e')
           ⇒ v1 ∈ lifting-2(F)|X,Prior(self)?init|(e')
           ⇒ (v1 = v2 ∈ B))))
10. v1 : B@i
11. v2 : B@i
12. single-valued-bag(init loc(e);B)@i
13. single-valued-classrel(es;X;A)@i
14. a : A
15. b : B
16. v2 = (F a b) ∈ B
17. ∀e':E. ((e' <loc e) ⇒ (∀w:B. (¬w ∈ lifting-2(F)|X,Prior(self)?init|(e'))))
18. b ↓∈ init loc(e)
19. a ∈ X(e)
20. a1 : A
21. b1 : B
22. v1 = (F a1 b1) ∈ B
23. e' : E
24. es-p-local-pred(es;λe'.(↓∃w:B. w ∈ lifting-2(F)|X,Prior(self)?init|(e'))) e e'
25. b1 ∈ lifting-2(F)|X,Prior(self)?init|(e')
26. a1 ∈ X(e)
27. a = a1 ∈ A
⊢ b1 = b ∈ B
BY
{ ((Assert ⌜False⌝⋅ THEN Auto)
   THEN All (RepUR ``es-p-local-pred``)
   THEN RepD
   THEN InstHyp [⌜e'⌝;⌜b1⌝] (-13)⋅
   THEN MaAuto) }

---

Latex:

---

Latex:

1.  Info  :  Type
2.  A  :  Type
3.  B  :  Type
4.  es  :  EO+(Info)
5.  F  :  A  {}\mrightarrow{}  B  {}\mrightarrow{}  B
6.  X  :  EClass(A)
7.  init  :  Id  {}\mrightarrow{}  bag(B)
8.  e  :  E@i
9.  \mforall{}e':E
          ((e'  <  e)
          {}\mRightarrow{}  (\mforall{}v1,v2:B.
                      (single-valued-bag(init  loc(e');B)
                      {}\mRightarrow{}  single-valued-classrel(es;X;A)
                      {}\mRightarrow{}  v2  \mmember{}  lifting-2(F)|X,Prior(self)?init|(e')
                      {}\mRightarrow{}  v1  \mmember{}  lifting-2(F)|X,Prior(self)?init|(e')
                      {}\mRightarrow{}  (v1  =  v2))))
10.  v1  :  B@i
11.  v2  :  B@i
12.  single-valued-bag(init  loc(e);B)@i
13.  single-valued-classrel(es;X;A)@i
14.  a  :  A
15.  b  :  B
16.  v2  =  (F  a  b)
17.  \mforall{}e':E.  ((e'  <loc  e)  {}\mRightarrow{}  (\mforall{}w:B.  (\mneg{}w  \mmember{}  lifting-2(F)|X,Prior(self)?init|(e'))))
18.  b  \mdownarrow{}\mmember{}  init  loc(e)
19.  a  \mmember{}  X(e)
20.  a1  :  A
21.  b1  :  B
22.  v1  =  (F  a1  b1)
23.  e'  :  E
24.  es-p-local-pred(es;\mlambda{}e'.(\mdownarrow{}\mexists{}w:B.  w  \mmember{}  lifting-2(F)|X,Prior(self)?init|(e')))  e  e'
25.  b1  \mmember{}  lifting-2(F)|X,Prior(self)?init|(e')
26.  a1  \mmember{}  X(e)
27.  a  =  a1
\mvdash{}  b1  =  b


By

---

Latex:
((Assert  \mkleeneopen{}False\mkleeneclose{}\mcdot{}  THEN  Auto)
  THEN  All  (RepUR  ``es-p-local-pred``)
  THEN  RepD
  THEN  InstHyp  [\mkleeneopen{}e'\mkleeneclose{};\mkleeneopen{}b1\mkleeneclose{}]  (-13)\mcdot{}
  THEN  MaAuto)

---

Home Index