---

Step * 1 1 1 3 of Lemma es-interface-extensionality


1. A : Type
2. v : bag(A)@i
3. v1 : bag(A)@i
4. (#(v) + 1) ≤ 1
5. (#(v1) + 1) ≤ 1
6. False ⇒ False ⇒ (only(v) = only(v1) ∈ A)@i
7. False ⇒ False@i
8. False ⇐ False@i
⊢ v = v1 ∈ bag(A)
BY
{ (RWO "bag-size-zero" 0 THEN Auto)⋅ }

---

Latex:



1.  A  :  Type
2.  v  :  bag(A)@i
3.  v1  :  bag(A)@i
4.  (\#(v)  +  1)  \mleq{}  1
5.  (\#(v1)  +  1)  \mleq{}  1
6.  False  {}\mRightarrow{}  False  {}\mRightarrow{}  (only(v)  =  only(v1))@i
7.  False  {}\mRightarrow{}  False@i
8.  False  \mLeftarrow{}{}  False@i
\mvdash{}  v  =  v1


By

(RWO  "bag-size-zero"  0  THEN  Auto)\mcdot{}

---

Home Index