---

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