proposition: Lemma head_of_notNil : forall (l : list A) a (lne: l <> nil), head l = Some a -> proj1_sig (head_notNil lne) = a.
proof: Proof. intros. destruct l; try discr. simpl; inversion H; trivial. Qed.
imports: CoLoR(LogicUtil EqUtil RelUtil BoolUtil NatUtil) Coq(Setoid SetoidList FunInd)