proposition: Lemma occur_app : forall x l m, occur x (l ++ m) = occur x l + occur x m.
proof: Proof. induction l; simpl; intros. refl. rewrite IHl. unfold delta. case (eq_dec x a); intro; lia. Qed.
imports: CoLoR(ListUtil NatUtil LogicUtil)