Step
*
1
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 : A@i
14. y : A@i
⊢ x ↓∈ xs
⇒ y ↓∈ xs
⇒ (x = y ∈ A)
BY
{ ((Subst' xs ~ {only(xs)} 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 : A@i
14. y : A@i
\mvdash{} x \mdownarrow{}\mmember{} xs {}\mRightarrow{} y \mdownarrow{}\mmember{} xs {}\mRightarrow{} (x = y)
By
Latex:
((Subst' xs \msim{} \{only(xs)\} 0 THENA (BLemma `bag-size-one` THEN Auto))
THEN RWO "bag-member-single" 0
THEN EAuto 1)\mcdot{}
Home
Index