---

Step * of Lemma append-cancellation-right

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

---

Latex:

---

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


By

---

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

---

Home Index