---

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