---

Step * 1 2 1 2 of Lemma assert_of_bpermr


1. s : DSet
2. a1 : |s|
3. as' : |s| List
4. a : ∀bs:|s| List. (↑(as' ≡b bs) ⇐⇒ as' ≡(|s|) bs)
5. bs : |s| List
6. [a1 / as'] ≡(|s|) bs
⊢ (↑(a1 ∈b bs)) c∧ (as' ≡(|s|) (bs \ a1))
BY
{ (FLemma `cons_permr_mem` [(-1)] THEN Auto) }

1
1. s : DSet
2. a1 : |s|
3. as' : |s| List
4. a : ∀bs:|s| List. (↑(as' ≡b bs) ⇐⇒ as' ≡(|s|) bs)
5. bs : |s| List
6. [a1 / as'] ≡(|s|) bs
7. ↑(a1 ∈b bs)
8. ↑(a1 ∈b bs)
⊢ as' ≡(|s|) (bs \ a1)

---

Latex:

---

Latex:

1.  s  :  DSet
2.  a1  :  |s|
3.  as'  :  |s|  List
4.  a  :  \mforall{}bs:|s|  List.  (\muparrow{}(as'  \mequiv{}\msubb{}  bs)  \mLeftarrow{}{}\mRightarrow{}  as'  \mequiv{}(|s|)  bs)
5.  bs  :  |s|  List
6.  [a1  /  as']  \mequiv{}(|s|)  bs
\mvdash{}  (\muparrow{}(a1  \mmember{}\msubb{}  bs))  c\mwedge{}  (as'  \mequiv{}(|s|)  (bs  \mbackslash{}  a1))


By

---

Latex:
(FLemma  `cons\_permr\_mem`  [(-1)]  THEN  Auto)

---

Home Index