---

Step * of Lemma cons_succ

∀[T:Type]
  ∀l:T List
    ∀[P:T ⟶ ℙ]
      ∀a,x:T.
        (y = succ(x) in [a / l]
        ⇒ P[y]
        ⇒ ((P[hd(l)]) supposing (0 < ||l|| and (x = a ∈ T)) ∧ y = succ(x) in l⇒ P[y] supposing ¬(x = a ∈ T)))
BY
{ (Unfold `l_succ` 0 THEN Auto) }

1
1. [T] : Type
2. l : T List
3. [P] : T ⟶ ℙ
4. a : T
5. x : T
6. ∀i:ℕ. (i + 1 < ||[a / l]|| ⇒ ([a / l][i] = x ∈ T) ⇒ P[[a / l][i + 1]])
7. x = a ∈ T
8. 0 < ||l||
⊢ P[hd(l)]

2
1. [T] : Type
2. l : T List
3. [P] : T ⟶ ℙ
4. a : T
5. x : T
6. ∀i:ℕ. (i + 1 < ||[a / l]|| ⇒ ([a / l][i] = x ∈ T) ⇒ P[[a / l][i + 1]])
7. (P[hd(l)]) supposing (0 < ||l|| and (x = a ∈ T))
8. ¬(x = a ∈ T)
9. i : ℕ
10. i + 1 < ||l||
11. l[i] = x ∈ T
⊢ P[l[i + 1]]

---

Latex:

---

Latex:
\mforall{}[T:Type]
    \mforall{}l:T  List
        \mforall{}[P:T  {}\mrightarrow{}  \mBbbP{}]
            \mforall{}a,x:T.
                (y  =  succ(x)  in  [a  /  l]
                {}\mRightarrow{}  P[y]
                {}\mRightarrow{}  ((P[hd(l)])  supposing  (0  <  ||l||  and  (x  =  a))  \mwedge{}  y  =  succ(x)  in  l{}\mRightarrow{}  P[y]  supposing  \mneg{}(x  =  a\000C)))


By

---

Latex:
(Unfold  `l\_succ`  0  THEN  Auto)

---

Home Index