proposition: Lemma add_add_eq : forall k l, E.eq k l -> forall (x y : A) m, Equal (add k x (add l y m)) (add k x m).
proof: Proof. intros k l kl x y m. unfold Equal. intro k'. rewrite !add_o. destruct (eq_dec k k'); destruct (eq_dec l k'); try refl. absurd (E.eq k k'). hyp. trans l; hyp. Qed.
imports: Coq(FMaps FSetInterface) CoLoR(LogicUtil RelUtil BoolUtil ListUtil FSetUtil)