proposition: Lemma SubEnsembleInsertReplaceKey : forall (kv : Key * Value) (r : Ensemble (Key * Value)), SubEnsembleInsert kv r (EnsembleReplaceKey kv r).
proof: Proof. unfold SubEnsembleInsert, EnsembleInsert, EnsembleReplaceKey, EnsembleRemoveKey; intros; intuition. Qed.
imports: Coq.Sets.Ensembles