---

Step * 1 of Lemma last-concat-non-null


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

---

Latex:

---

Latex:

1.  T  :  Type
\mvdash{}  ((\mneg{}True)  \mwedge{}  (last([])  =  last(last([]))))  supposing  ((\mneg{}\muparrow{}null(last([])))  and  (\mneg{}True))


By

---

Latex:
Auto

---

Home Index