proposition: Lemma occur_notin : forall x l, occur x l = 0 -> ~In x l.
proof: Proof. induction l; simpl. do 2 intro. contr. unfold delta. case (eq_dec x a); intros. discr. intro. destruct H0. subst a. cong. intuition. Qed.
imports: CoLoR(ListUtil NatUtil LogicUtil)