---

Step * 1 1 1 of Lemma list_append_singleton_ind

.....basecase..... 
1. [T] : Type
2. [Q] : (T List) ⟶ ℙ
3. Q[[]]
4. ∀ys:T List. ∀x:T.  (Q[ys] ⇒ Q[ys @ [x]])
⊢ ∀l:T List. ((||l|| = 0 ∈ ℕ) ⇒ Q[l])
BY
{ ((((Auto THEN Subst l = [] ∈ (T List) 0) THEN Auto) THEN BackThruLemma `length_zero`) THEN TACTIC:Auto) }

---

Latex:

---

Latex:
.....basecase..... 
1.  [T]  :  Type
2.  [Q]  :  (T  List)  {}\mrightarrow{}  \mBbbP{}
3.  Q[[]]
4.  \mforall{}ys:T  List.  \mforall{}x:T.    (Q[ys]  {}\mRightarrow{}  Q[ys  @  [x]])
\mvdash{}  \mforall{}l:T  List.  ((||l||  =  0)  {}\mRightarrow{}  Q[l])


By

---

Latex:
((((Auto  THEN  Subst  l  =  []  0)  THEN  Auto)  THEN  BackThruLemma  `length\_zero`)  THEN  TACTIC:Auto)

---

Home Index