---

Step * of Lemma append_back_nil

∀[T:Type]. ∀[as:T List].  (as @ [] ~ as)
BY
{ (UnivCD THENA Auto) }

1
1. T : Type
2. as : T List
⊢ as @ [] ~ as

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[as:T  List].    (as  @  []  \msim{}  as)


By

---

Latex:
(UnivCD  THENA  Auto)

---

Home Index