---

Step * of Lemma append_comm

∀T:Type. ∀as,bs:T List.  ((as @ bs) ≡(T) (bs @ as))
BY
{ ((D 0 THENM D 0) THENA Auto) }

1
1. T : Type
2. as : T List
⊢ ∀bs:T List. ((as @ bs) ≡(T) (bs @ as))

---

Latex:

---

Latex:
\mforall{}T:Type.  \mforall{}as,bs:T  List.    ((as  @  bs)  \mequiv{}(T)  (bs  @  as))


By

---

Latex:
((D  0  THENM  D  0)  THENA  Auto)

---

Home Index