proposition: Lemma add_eq_d : forall m x y, x = y -> find y (add x m.(default) m) = None.
proof: Proof. intros. simpl. rewrite add_d_rem. case_eq (find y (remove x m)); auto. intros. apply find_2 in H0. unfold MapsTo, Raw.MapsTo in H0. assert (exists e, InA (Raw.eqk (elt:=elt)) (y, e) (remove x m).(this)). exists e. apply Raw.InA_eqke_eqk in H0. auto. rewrite <- Raw.In_alt in H1; auto. contradict H1. apply remove_1; auto. apply key_comp. Qed.
imports: Bool OrderedType SMT_classes ProofIrrelevance