---

Step * 2 of Lemma es-interface-pair-prior-programmable


1. Info : Type
2. A : Type
3. B : Type
4. X : EClass(A)
5. Y : EClass(B)
6. Singlevalued(X)
7. ys : bag(B)@i
8. xs : bag(A)@i
9. (#(ys) =z 1) ∈ 𝔹
10. #(ys) = 1 ∈ ℤ
11. (#(xs) =z 1) ∈ 𝔹
12. #(xs) = 1 ∈ ℤ
13. x : B@i
14. y : B@i
⊢ x ↓∈ ys ⇒ y ↓∈ ys ⇒ (x = y ∈ B)
BY
{ ((Subst' ys ~ {only(ys)} 0 THENA (BLemma `bag-size-one` THEN Auto)) THEN RWO "bag-member-single" 0 THEN EAuto 1) }

---

Latex:

---

Latex:

1.  Info  :  Type
2.  A  :  Type
3.  B  :  Type
4.  X  :  EClass(A)
5.  Y  :  EClass(B)
6.  Singlevalued(X)
7.  ys  :  bag(B)@i
8.  xs  :  bag(A)@i
9.  (\#(ys)  =\msubz{}  1)  \mmember{}  \mBbbB{}
10.  \#(ys)  =  1
11.  (\#(xs)  =\msubz{}  1)  \mmember{}  \mBbbB{}
12.  \#(xs)  =  1
13.  x  :  B@i
14.  y  :  B@i
\mvdash{}  x  \mdownarrow{}\mmember{}  ys  {}\mRightarrow{}  y  \mdownarrow{}\mmember{}  ys  {}\mRightarrow{}  (x  =  y)


By

---

Latex:
((Subst'  ys  \msim{}  \{only(ys)\}  0  THENA  (BLemma  `bag-size-one`  THEN  Auto))
  THEN  RWO  "bag-member-single"  0
  THEN  EAuto  1)

---

Home Index