fact: Fixpoint inits {A} (l: L A): L (L A) := match l with | one x => one (one x) | cons h t => cons (one h) (map (cons h) (inits t)) end.
imports: Coq.Unicode.Utf8 Coq.Lists.List Coq.Setoids.Setoid Coq.Classes.Morphisms Coq.Sorting.Permutation