---

Step * 1 of Lemma cons_permr_mem


1. s : DSet
2. a : |s|
3. as : |s| List
4. bs : |s| List
5. [a / as] ≡(|s|) bs
⊢ ↑(a ∈b bs)
BY
{ ((((InvertRel 5 THENA Auto{1,3}-1) THEN D 5) THEN D 6) THEN (BLemma `mem_iff_exists` THENA Auto)) }

1
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|)

---

Latex:

---

Latex:

1.  s  :  DSet
2.  a  :  |s|
3.  as  :  |s|  List
4.  bs  :  |s|  List
5.  [a  /  as]  \mequiv{}(|s|)  bs
\mvdash{}  \muparrow{}(a  \mmember{}\msubb{}  bs)


By

---

Latex:
((((InvertRel  5  THENA  Auto\{1,3\}-1)  THEN  D  5)  THEN  D  6)  THEN  (BLemma  `mem\_iff\_exists`  THENA  Auto))

---

Home Index