proposition: Lemma add_add_Equiv : Reflexive eq -> forall k l x y m, Equiv eq (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 heq k l x y m. destruct (eq_dec k l). apply add_add_eq_Equiv; hyp. apply add_add_neq_Equiv; hyp. Qed.
imports: Coq(FMaps FSetInterface) CoLoR(LogicUtil RelUtil BoolUtil ListUtil FSetUtil)