---

Step * 1 2 2 of Lemma bag-extensionality-no-repeats


1. T : Type
2. ∀x,y:T.  Dec(x = y ∈ T)
3. as : T List
4. bs : T List
5. L1 : T List
6. L1 = as ∈ (as,bs:T List//permutation(T;as;bs))
7. L1 ∈ T List
8. as ∈ T List
9. permutation(T;L1;as)
10. no_repeats(T;L1)
11. L : T List
12. L = bs ∈ (as,bs:T List//permutation(T;as;bs))
13. L ∈ T List
14. bs ∈ T List
15. permutation(T;L;bs)
16. no_repeats(T;L)
17. ∀x:T. uiff(x ↓∈ as;x ↓∈ bs)
18. x : T
19. (x ∈ as)
20. x ↓∈ as supposing x ↓∈ bs
21. x ↓∈ bs
⊢ (x ∈ bs)
BY
{ (InstLemma `bag-member-list-member` [⌜T⌝;⌜bs⌝;⌜bs⌝;⌜x⌝]⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  \mforall{}x,y:T.    Dec(x  =  y)
3.  as  :  T  List
4.  bs  :  T  List
5.  L1  :  T  List
6.  L1  =  as
7.  L1  \mmember{}  T  List
8.  as  \mmember{}  T  List
9.  permutation(T;L1;as)
10.  no\_repeats(T;L1)
11.  L  :  T  List
12.  L  =  bs
13.  L  \mmember{}  T  List
14.  bs  \mmember{}  T  List
15.  permutation(T;L;bs)
16.  no\_repeats(T;L)
17.  \mforall{}x:T.  uiff(x  \mdownarrow{}\mmember{}  as;x  \mdownarrow{}\mmember{}  bs)
18.  x  :  T
19.  (x  \mmember{}  as)
20.  x  \mdownarrow{}\mmember{}  as  supposing  x  \mdownarrow{}\mmember{}  bs
21.  x  \mdownarrow{}\mmember{}  bs
\mvdash{}  (x  \mmember{}  bs)


By

---

Latex:
(InstLemma  `bag-member-list-member`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}bs\mkleeneclose{};\mkleeneopen{}bs\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]\mcdot{}  THEN  Auto)

---

Home Index