proposition: Lemma add_add_eq_Equiv : Reflexive eq -> forall k l, E.eq k l -> forall x y m, Equiv eq (add k x (add l y m)) (add k x m).
proof: Proof. intros heq k l kl x y m. apply Equal_Equiv. intuition. apply add_add_eq. hyp. Qed.
imports: Coq(FMaps FSetInterface) CoLoR(LogicUtil RelUtil BoolUtil ListUtil FSetUtil)