---

Step * of Lemma append-cancellation

∀[T:Type]. ∀[as,as',bs,cs:T List].
  (cs = bs ∈ (T List)) supposing (((as @ cs) = (as' @ bs) ∈ (T List)) and (||as|| = ||as'|| ∈ ℤ))
BY
{ (Auto
   THEN (InstLemma `general-append-cancellation` [⌜T⌝; ⌜as⌝; ⌜as'⌝; ⌜cs⌝; ⌜bs⌝])⋅
   THEN Auto
   THEN OrLeft
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[as,as',bs,cs:T  List].
    (cs  =  bs)  supposing  (((as  @  cs)  =  (as'  @  bs))  and  (||as||  =  ||as'||))


By

---

Latex:
(Auto
  THEN  (InstLemma  `general-append-cancellation`  [\mkleeneopen{}T\mkleeneclose{};  \mkleeneopen{}as\mkleeneclose{};  \mkleeneopen{}as'\mkleeneclose{};  \mkleeneopen{}cs\mkleeneclose{};  \mkleeneopen{}bs\mkleeneclose{}])\mcdot{}
  THEN  Auto
  THEN  OrLeft
  THEN  Auto)

---

Home Index