---

Step * 1 2 1 1 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 ∈b bs)) c∧ (as' ≡(|s|) (bs \ a1))
⊢ [a1 / as'] ≡(|s|) bs
BY
{ (D (-1) THEN (RewriteWith [(-1)] ``cons_remove1_permr`` 0 THENA 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 ∈b bs)
7. as' ≡(|s|) (bs \ a1)
⊢ bs ≡(|s|) bs

---

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.  (\muparrow{}(a1  \mmember{}\msubb{}  bs))  c\mwedge{}  (as'  \mequiv{}(|s|)  (bs  \mbackslash{}  a1))
\mvdash{}  [a1  /  as']  \mequiv{}(|s|)  bs


By

---

Latex:
(D  (-1)  THEN  (RewriteWith  [(-1)]  ``cons\_remove1\_permr``  0  THENA  Auto))

---

Home Index