---

Step * 1 of Lemma append_iseg


1. T : Type
2. as : T List
3. bs : T List
4. cs : T List
5. l : T List
6. (as @ cs) = ((as @ bs) @ l) ∈ (T List)
⊢ cs = (bs @ l) ∈ (T List)
BY
{ (((RWO "append_assoc" (-1)) THENA Auto) THEN (FLemma `append-cancellation` [(-1)]) THEN Auto) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  as  :  T  List
3.  bs  :  T  List
4.  cs  :  T  List
5.  l  :  T  List
6.  (as  @  cs)  =  ((as  @  bs)  @  l)
\mvdash{}  cs  =  (bs  @  l)


By

---

Latex:
(((RWO  "append\_assoc"  (-1))  THENA  Auto)  THEN  (FLemma  `append-cancellation`  [(-1)])  THEN  Auto)

---

Home Index