proposition: Lemma Permutation_ne_tl_length (x y: L): Permutation x y → length (tl x) = length (tl y).
proof: Proof. intro H. apply eq_add_S. do 2 rewrite tl_length. rewrite H. reflexivity. Qed.
imports: Coq.Unicode.Utf8 Coq.Lists.List Coq.Setoids.Setoid Coq.Classes.Morphisms Coq.Sorting.Permutation