Step
*
1
of Lemma
append_comm
1. T : Type
2. as : T List
⊢ ∀bs:T List. ((as @ bs) ≡(T) (bs @ as))
BY
{ (New [`a'; `as\''] (ListInd 2) THEN AbReduce 0) }
1
1. T : Type
⊢ ∀bs:T List. (bs ≡(T) (bs @ []))
2
1. T : Type
2. a1 : T
3. as' : T List
4. a : ∀bs:T List. ((as' @ bs) ≡(T) (bs @ as'))
⊢ ∀bs:T List. ([a1 / (as' @ bs)] ≡(T) (bs @ [a1 / as']))
Latex:
Latex:
1. T : Type
2. as : T List
\mvdash{} \mforall{}bs:T List. ((as @ bs) \mequiv{}(T) (bs @ as))
By
Latex:
(New [`a'; `as\mbackslash{}''] (ListInd 2) THEN AbReduce 0)
Home
Index