proposition: Lemma head_notNil : forall (l : list A) (lne : l <> nil), {a : A | head l = Some a}.
proof: Proof. destruct l. tauto. exists a; auto. Defined.
imports: CoLoR(LogicUtil EqUtil RelUtil BoolUtil NatUtil) Coq(Setoid SetoidList FunInd)