---

Step * of Lemma append_functionality_wrt_permr

∀T:Type. ∀as,as',bs,bs':T List.  ((as ≡(T) as') ⇒ (bs ≡(T) bs') ⇒ ((as @ bs) ≡(T) (as' @ bs')))
BY
{ (UnivCD THENA Auto) }

1
1. T : Type
2. as : T List
3. as' : T List
4. bs : T List
5. bs' : T List
6. as ≡(T) as'
7. bs ≡(T) bs'
⊢ (as @ bs) ≡(T) (as' @ bs')

---

Latex:

---

Latex:
\mforall{}T:Type.  \mforall{}as,as',bs,bs':T  List.    ((as  \mequiv{}(T)  as')  {}\mRightarrow{}  (bs  \mequiv{}(T)  bs')  {}\mRightarrow{}  ((as  @  bs)  \mequiv{}(T)  (as'  @  bs')))


By

---

Latex:
(UnivCD  THENA  Auto)

---

Home Index