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