fact: Fixpoint foldr1 (f: T → T → T) (a: L): T := match a with | one x => x | cons x y => f x (foldr1 f y) end.
imports: Coq.Unicode.Utf8 Coq.Lists.List Coq.Setoids.Setoid Coq.Classes.Morphisms Coq.Sorting.Permutation