Step
*
of Lemma
append_comm_1
∀T:Type. ∀a:T. ∀as:T List.  ((as @ [a]) ≡(T) ([a] @ as))
BY
{ (Auto THEN ListInd 3 THEN AbReduce 0) }
1
1. T : Type
2. a : T
⊢ [a] ≡(T) [a]
2
1. T : Type
2. a : T
3. u : T
4. v : T List
5. (v @ [a]) ≡(T) ([a] @ v)
⊢ [u / (v @ [a])] ≡(T) [a; [u / v]]
Latex:
Latex:
\mforall{}T:Type.  \mforall{}a:T.  \mforall{}as:T  List.    ((as  @  [a])  \mequiv{}(T)  ([a]  @  as))
By
Latex:
(Auto  THEN  ListInd  3  THEN  AbReduce  0)
Home
Index