---

Step * of Lemma list_append_singleton_ind

∀[T:Type]. ∀[Q:(T List) ⟶ ℙ].  (Q[[]] ⇒ (∀ys:T List. ∀x:T.  (Q[ys] ⇒ Q[ys @ [x]])) ⇒ {∀zs:T List. Q[zs]})
BY
{ (Auto THEN Unfold `guard` 0) }

1
1. [T] : Type
2. [Q] : (T List) ⟶ ℙ
3. Q[[]]
4. ∀ys:T List. ∀x:T.  (Q[ys] ⇒ Q[ys @ [x]])
⊢ ∀zs:T List. Q[zs]

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[Q:(T  List)  {}\mrightarrow{}  \mBbbP{}].
    (Q[[]]  {}\mRightarrow{}  (\mforall{}ys:T  List.  \mforall{}x:T.    (Q[ys]  {}\mRightarrow{}  Q[ys  @  [x]]))  {}\mRightarrow{}  \{\mforall{}zs:T  List.  Q[zs]\})


By

---

Latex:
(Auto  THEN  Unfold  `guard`  0)

---

Home Index