---

Step * 1 of Lemma list_append_ind


1. [T] : Type
2. [Q] : (T List) ⟶ ℙ
3. Q[[]]@i
4. ∀x:T. Q[[x]]@i
5. ∀ys,ys':T List.  (Q[ys] ⇒ Q[ys'] ⇒ Q[ys @ ys'])@i
6. u : T@i
7. v : T List@i
8. Q[v]@i
⊢ Q[[u / v]]
BY
{ (RWH cons_to_appendC 0 THEN Auto) }

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  [Q]  :  (T  List)  {}\mrightarrow{}  \mBbbP{}
3.  Q[[]]@i
4.  \mforall{}x:T.  Q[[x]]@i
5.  \mforall{}ys,ys':T  List.    (Q[ys]  {}\mRightarrow{}  Q[ys']  {}\mRightarrow{}  Q[ys  @  ys'])@i
6.  u  :  T@i
7.  v  :  T  List@i
8.  Q[v]@i
\mvdash{}  Q[[u  /  v]]


By

---

Latex:
(RWH  cons\_to\_appendC  0  THEN  Auto)

---

Home Index