---

Step * of Lemma diff_functionality_wrt_permr

∀s:DSet. ∀as,as',bs,bs':|s| List.  ((as ≡(|s|) as') ⇒ (bs ≡(|s|) bs') ⇒ ((as - bs) ≡(|s|) (as' - bs')))
BY
{ Auto }

1
1. s : DSet
2. as : |s| List
3. as' : |s| List
4. bs : |s| List
5. bs' : |s| List
6. as ≡(|s|) as'
7. bs ≡(|s|) bs'
⊢ (as - bs) ≡(|s|) (as' - bs')

---

Latex:

---

Latex:
\mforall{}s:DSet.  \mforall{}as,as',bs,bs':|s|  List.
    ((as  \mequiv{}(|s|)  as')  {}\mRightarrow{}  (bs  \mequiv{}(|s|)  bs')  {}\mRightarrow{}  ((as  -  bs)  \mequiv{}(|s|)  (as'  -  bs')))


By

---

Latex:
Auto

---

Home Index