---

Step * 1 2 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. ||cs|| = ||ds|| ∈ ℤ
⊢ False
BY
{ (((HypSubst (-2) (-1)) THENA Auto) THEN (Reduce (-1)) THEN (RWO "length_append" (-1)) THEN 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.  ||cs||  =  ||ds||
\mvdash{}  False


By

---

Latex:
(((HypSubst  (-2)  (-1))  THENA  Auto)  THEN  (Reduce  (-1))  THEN  (RWO  "length\_append"  (-1))  THEN  Auto')

---

Home Index