proposition: Lemma in_head_tail : forall a (l : list A), In a l -> Some a = head l \/ In a (tail l).
proof: Proof. induction l; intros; inversion H. left; simpl; rewrite H0; trivial. right; trivial. Qed.
imports: CoLoR(LogicUtil EqUtil RelUtil BoolUtil NatUtil) Coq(Setoid SetoidList FunInd)