---

Step * 4 of Lemma prior-as-rec-bind-class-in-property


1. Info : Type
2. A : Type
3. X : EClass(A)
4. y1 : Unit
5. a : bag(A) + (bag(A)?)
6. es : EO+(Info)
7. e : E
8. x : bag(A)?
9. x ∈ λes,e. ∪x∈Lift(X) es e.{inl x} || λes,e. ∪x∈Null es e.{inr x }(e)
10. a ↓∈ {inr x }
11. w : bag(A) + (bag(A)?)
12. e ∈ E
13. w ∈ prior-as-rec-bind-class-in(X;a)(e)@i
⊢ False
BY
{ (BagMemberD (-4)
   THEN (MaUseClassRel (-5)
         THENA (Unfold `eclass` 0 THEN Auto THEN Try (Fold `eclass` 0) THEN Auto THEN RepUR ``null-class`` 0 THEN Auto)
         )
   THEN MaUseClassRel (-5)
   THEN BagMemberD (-5)
   THEN SquashExRepD
   THEN Fold `classrel` (-6)
   THEN Try (OnSomeHyp (\h.RWO "null-class-property" h THEN Auto)))⋅ }

1
1. Info : Type
2. A : Type
3. X : EClass(A)
4. y1 : Unit
5. a : bag(A) + (bag(A)?)
6. es : EO+(Info)
7. e : E
8. x : bag(A)?
9. x1 : bag(A)
10. x1 ∈ Lift(X)(e)
11. x ↓∈ {inl x1}
12. a = (inr x ) ∈ (bag(A) + (bag(A)?))
13. w : bag(A) + (bag(A)?)
14. e ∈ E
15. w ∈ prior-as-rec-bind-class-in(X;a)(e)@i
⊢ False

---

Latex:

---

Latex:

1.  Info  :  Type
2.  A  :  Type
3.  X  :  EClass(A)
4.  y1  :  Unit
5.  a  :  bag(A)  +  (bag(A)?)
6.  es  :  EO+(Info)
7.  e  :  E
8.  x  :  bag(A)?
9.  x  \mmember{}  \mlambda{}es,e.  \mcup{}x\mmember{}Lift(X)  es  e.\{inl  x\}  ||  \mlambda{}es,e.  \mcup{}x\mmember{}Null  es  e.\{inr  x  \}(e)
10.  a  \mdownarrow{}\mmember{}  \{inr  x  \}
11.  w  :  bag(A)  +  (bag(A)?)
12.  e  \mmember{}  E
13.  w  \mmember{}  prior-as-rec-bind-class-in(X;a)(e)@i
\mvdash{}  False


By

---

Latex:
(BagMemberD  (-4)
  THEN  (MaUseClassRel  (-5)
              THENA  (Unfold  `eclass`  0
                            THEN  Auto
                            THEN  Try  (Fold  `eclass`  0)
                            THEN  Auto
                            THEN  RepUR  ``null-class``  0
                            THEN  Auto)
              )
  THEN  MaUseClassRel  (-5)
  THEN  BagMemberD  (-5)
  THEN  SquashExRepD
  THEN  Fold  `classrel`  (-6)
  THEN  Try  (OnSomeHyp  (\mbackslash{}h.RWO  "null-class-property"  h  THEN  Auto)))\mcdot{}

---

Home Index