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