proposition: Lemma notin_occur : forall x l, ~In x l -> occur x l = 0.
proof: Proof. induction l; simpl; intros. refl. unfold delta. case (eq_dec x a); intro. subst a. absurd (x=x \/ In x l). exact H. auto. apply IHl. intro. apply H. auto. Qed.
imports: CoLoR(ListUtil NatUtil LogicUtil)