∀T:Type. ∀as:T List. ((as ≡(T) [])
(as = [] ∈ (T List)))
{ (((D 0 THENM D 0) THENM D 2) THENA Auto) }
1. T : Type
⊢ ([] ≡(T) [])
([] = [] ∈ (T List))
2. u : T
3. v : T List
⊢ ([u / v] ≡(T) [])
([u / v] = [] ∈ (T List))