---

Step * 1 of Lemma imax-bag_wf


1. ℤ List ∈ Type
2. ∀as,b1:ℤ List.  (permutation(ℤ;as;b1) ∈ Type)
3. ∀as:ℤ List. permutation(ℤ;as;as)
4. a : Base
5. b : Base
6. c : a = b ∈ pertype(λas,bs. ((as ∈ ℤ List) ∧ (bs ∈ ℤ List) ∧ permutation(ℤ;as;bs)))
7. a ∈ ℤ List
8. b ∈ ℤ List
9. permutation(ℤ;a;b)
10. 0 < ||a||
⊢ set-equal(ℤ;a;b)
BY
{ ((FLemma `member-permutation` [-2] THENA Auto) THEN Fold `set-equal` (-1) THEN Auto)⋅ }

---

Latex:

---

Latex:

1.  \mBbbZ{}  List  \mmember{}  Type
2.  \mforall{}as,b1:\mBbbZ{}  List.    (permutation(\mBbbZ{};as;b1)  \mmember{}  Type)
3.  \mforall{}as:\mBbbZ{}  List.  permutation(\mBbbZ{};as;as)
4.  a  :  Base
5.  b  :  Base
6.  c  :  a  =  b
7.  a  \mmember{}  \mBbbZ{}  List
8.  b  \mmember{}  \mBbbZ{}  List
9.  permutation(\mBbbZ{};a;b)
10.  0  <  ||a||
\mvdash{}  set-equal(\mBbbZ{};a;b)


By

---

Latex:
((FLemma  `member-permutation`  [-2]  THENA  Auto)  THEN  Fold  `set-equal`  (-1)  THEN  Auto)\mcdot{}

---

Home Index