proposition: Lemma in_occur : forall x l, In x l -> occur x l > 0.
proof: Proof. induction l; simpl; intros. contr. unfold delta. case (eq_dec x a); intro. lia. destruct H. subst a. cong. auto. Qed.
imports: CoLoR(ListUtil NatUtil LogicUtil)