---

Step * 1 1 of Lemma general-append-cancellation


1. T : Type
2. u : T
3. v : T List
4. cs : T List
5. ds : T List
6. cs = [u / (v @ ds)] ∈ (T List)
7. 0 = (||v|| + 1) ∈ ℤ
⊢ False
BY
{ Auto' }

---

Latex:

---

Latex:

1.  T  :  Type
2.  u  :  T
3.  v  :  T  List
4.  cs  :  T  List
5.  ds  :  T  List
6.  cs  =  [u  /  (v  @  ds)]
7.  0  =  (||v||  +  1)
\mvdash{}  False


By

---

Latex:
Auto'

---

Home Index