proposition: Lemma list_decompose_head : forall (l : list A) el (lne: l <> nil), head l = Some el -> l = el :: tail l.
proof: Proof. intros. destruct l. discr. inversion H. rewrite <- H1; trivial. Qed.
imports: CoLoR(LogicUtil EqUtil RelUtil BoolUtil NatUtil) Coq(Setoid SetoidList FunInd)