fact: Fixpoint from_list (x: T) (xs: list T): L := match xs with | nil => one x | List.cons h t => cons x (from_list h t) end.
imports: Coq.Unicode.Utf8 Coq.Lists.List Coq.Setoids.Setoid Coq.Classes.Morphisms Coq.Sorting.Permutation