---

Step * of Lemma remove1_functionality_wrt_permr

∀s:DSet. ∀a,a':|s|. ∀bs,bs':|s| List.  ((a = a' ∈ |s|) ⇒ (bs ≡(|s|) bs') ⇒ ((bs \ a) ≡(|s|) (bs' \ a')))
BY
{ Auto }

1
1. s : DSet
2. a : |s|
3. a' : |s|
4. bs : |s| List
5. bs' : |s| List
6. a = a' ∈ |s|
7. bs ≡(|s|) bs'
⊢ (bs \ a) ≡(|s|) (bs' \ a')

---

Latex:

---

Latex:
\mforall{}s:DSet.  \mforall{}a,a':|s|.  \mforall{}bs,bs':|s|  List.    ((a  =  a')  {}\mRightarrow{}  (bs  \mequiv{}(|s|)  bs')  {}\mRightarrow{}  ((bs  \mbackslash{}  a)  \mequiv{}(|s|)  (bs'  \mbackslash{}  a')))


By

---

Latex:
Auto

---

Home Index