proposition: Lemma decomp_eq (l: L): l = from_list (head l) (tail l).
proof: Proof. Proof with auto. induction l... destruct l... simpl in *. rewrite IHl... Qed.
imports: Coq.Unicode.Utf8 Coq.Lists.List Coq.Setoids.Setoid Coq.Classes.Morphisms Coq.Sorting.Permutation