proposition: Lemma add_add : forall k l (x y : A) m, Equal (add k x (add l y m)) (if eq_dec k l then add k x m else add l y (add k x m)).
proof: Proof. intros k l x y m. destruct (eq_dec k l). apply add_add_eq; hyp. apply add_add_neq; hyp. Qed.
imports: Coq(FMaps FSetInterface) CoLoR(LogicUtil RelUtil BoolUtil ListUtil FSetUtil)