---

Step * of Lemma last-concat-non-null

∀[T:Type]. ∀[ll:T List List].
  ((¬↑null(concat(ll))) ∧ (last(concat(ll)) = last(last(ll)) ∈ T)) supposing ((¬↑null(last(ll))) and (¬↑null(ll)))
BY
{ (InductionOnList THEN Reduce 0) }

1
1. T : Type
⊢ ((¬True) ∧ (last([]) = last(last([])) ∈ T)) supposing ((¬↑null(last([]))) and (¬True))

2
1. T : Type
2. u : T List
3. v : T List List
4. ((¬↑null(concat(v))) ∧ (last(concat(v)) = last(last(v)) ∈ T)) supposing ((¬↑null(last(v))) and (¬↑null(v)))
⊢ ((¬↑null(concat([u / v]))) ∧ (last(concat([u / v])) = last(last([u / v])) ∈ T)) supposing 
     ((¬↑null(last([u / v]))) and 
     (¬False))

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[ll:T  List  List].
    ((\mneg{}\muparrow{}null(concat(ll)))  \mwedge{}  (last(concat(ll))  =  last(last(ll))))  supposing 
          ((\mneg{}\muparrow{}null(last(ll)))  and 
          (\mneg{}\muparrow{}null(ll)))


By

---

Latex:
(InductionOnList  THEN  Reduce  0)

---

Home Index