---

Step * 1 1 of Lemma cons_permr_mem


1. s : DSet
2. a : |s|
3. as : |s| List
4. bs : |s| List
5. ||bs|| = ||[a / as]|| ∈ ℤ
6. p : Sym(||bs||)
7. ∀i:ℕ||bs||. (bs[p.f i] = [a / as][i] ∈ |s|)
⊢ ∃n:ℕ||bs||. (bs[n] = a ∈ |s|)
BY
{ (((With 0 (D 7) THENM With p.f 0 (D 0)) THENM AbReduce (-1)) THEN Auto') }

---

Latex:

---

Latex:

1.  s  :  DSet
2.  a  :  |s|
3.  as  :  |s|  List
4.  bs  :  |s|  List
5.  ||bs||  =  ||[a  /  as]||
6.  p  :  Sym(||bs||)
7.  \mforall{}i:\mBbbN{}||bs||.  (bs[p.f  i]  =  [a  /  as][i])
\mvdash{}  \mexists{}n:\mBbbN{}||bs||.  (bs[n]  =  a)


By

---

Latex:
(((With  0  (D  7)  THENM  With  p.f  0  (D  0))  THENM  AbReduce  (-1))  THEN  Auto')

---

Home Index