---

Step * 2 1 1 2 2 1 of Lemma descending-append


1. [A] : Type
2. [<] : A ⟶ A ⟶ ℙ
3. L2 : A List
4. ∀i:ℕ-1. <[⊥;⊥]
5. ∀i:ℕ||L2|| - 1. <[L2[i + 1];L2[i]]
6. (<[hd(L2);last([])]) supposing (0 < ||L2|| and 0 < 0)
7. i : ℕ(0 + ||L2||) - 1
8. ¬i < -1
9. ¬0 < 0
⊢ <[L2[i + 1];L2[i]]
BY
{ (BHyp 5 THEN Auto) }

---

Latex:

---

Latex:

1.  [A]  :  Type
2.  [<]  :  A  {}\mrightarrow{}  A  {}\mrightarrow{}  \mBbbP{}
3.  L2  :  A  List
4.  \mforall{}i:\mBbbN{}-1.  <[\mbot{};\mbot{}]
5.  \mforall{}i:\mBbbN{}||L2||  -  1.  <[L2[i  +  1];L2[i]]
6.  (<[hd(L2);last([])])  supposing  (0  <  ||L2||  and  0  <  0)
7.  i  :  \mBbbN{}(0  +  ||L2||)  -  1
8.  \mneg{}i  <  -1
9.  \mneg{}0  <  0
\mvdash{}  <[L2[i  +  1];L2[i]]


By

---

Latex:
(BHyp  5  THEN  Auto)

---

Home Index