fact: Fixpoint init {a : Type} (x : a) (l : list a) := match l with | nil => nil | cons y nil => [x] | cons y ys => x :: init y ys end.
imports: Coq.Lists.List Equations(Equations) Equations.Type.EqDec Category.Lib Category.Theory.Coq.Functor Category.Theory.Coq.Applicative Category.Theory.Coq.Monad Category.Theory.Coq.Maybe Coq.Lists.List