proposition: Lemma succs_add : forall x y s g, succs x (add y s g) = if eq_dec y x then s else succs x g.
proof: Proof. intros x y s g. unfold succs at 1. rewrite add_o. destruct (eq_dec y x); refl. Qed.
imports: Coq(OrderedType) CoLoR(ListUtil FSetUtil FMapUtil RelUtil LogicUtil)