---

Step * of Lemma append_cancel_wrt_permutation

∀[A:Type]. ∀as,bs,cs:A List.  (permutation(A;as @ bs;as @ cs) ⇒ permutation(A;bs;cs))
BY
{ (InductionOnList THEN Reduce 0 THEN Auto THEN FLemma `cons_cancel_wrt_permutation` [-1] THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}as,bs,cs:A  List.    (permutation(A;as  @  bs;as  @  cs)  {}\mRightarrow{}  permutation(A;bs;cs))


By

---

Latex:
(InductionOnList  THEN  Reduce  0  THEN  Auto  THEN  FLemma  `cons\_cancel\_wrt\_permutation`  [-1]  THEN  Auto)

---

Home Index