---

Step * 1 1 1 2 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@i
6. #(v1) = 1 ∈ ℤ
7. False ⇒ True ⇒ (only(v) = only(v1) ∈ A)@i
8. False ⇒ True@i
9. False ⇐ True@i
⊢ v = v1 ∈ bag(A)
BY
{ (D -1 THEN Auto) }

---

Latex:



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


By

(D  -1  THEN  Auto)

---

Home Index