proposition: Lemma add_d_rem : forall m x, add x m.(default) m = remove x m.
proof: Proof. intros. unfold add, remove. specialize (raw_add_d_rem m.(sorted) x). intro. generalize (add_sorted m.(default) m.(sorted) x m.(default)). generalize (add_nodefault (nodefault m) (sorted m) x m.(default)). generalize (Raw.remove_sorted key_comp (sorted m) x). generalize (remove_nodefault (nodefault m) (sorted m) x). rewrite H. intros H4 H3 H2 H1. rewrite (proof_irrelevance _ H1 H3), (proof_irrelevance _ H2 H4). reflexivity. Qed.
imports: Bool OrderedType SMT_classes ProofIrrelevance