---

Step * 1 of Lemma append_back_nil


1. T : Type
2. as : T List
⊢ as @ [] ~ as
BY
{ ((ListInd 2 THEN AbReduce 0) THEN EqCD THEN Auto) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  as  :  T  List
\mvdash{}  as  @  []  \msim{}  as


By

---

Latex:
((ListInd  2  THEN  AbReduce  0)  THEN  EqCD  THEN  Auto)

---

Home Index