---

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


1. A : Type
2. v : bag(A)@i
3. v1 : bag(A)@i
4. #(v) ≤ 1@i
5. #(v1) ≤ 1@i
6. #(v) = 1 ∈ ℤ
7. #(v1) = 1 ∈ ℤ
8. True ⇐ True@i
9. True@i
10. only(v) = only(v1) ∈ A@i
⊢ v = v1 ∈ bag(A)
BY
{ (MoveToConcl (-1) THEN ElimBagSizeOne'⋅ THEN Reduce 0 THEN Auto) }

---

Latex:



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


By

(MoveToConcl  (-1)  THEN  ElimBagSizeOne'\mcdot{}  THEN  Reduce  0  THEN  Auto)

---

Home Index