proposition: Lemma AbsR_add_EnsembleReplace {A} : forall nr kv or v, EnsembleFMapEquivalence or nr -> StringIndexedMap.find (elt:=A) (fst kv) nr = Some v -> EnsembleFMapEquivalence (EnsembleReplace kv or) (StringIndexedMap.add (fst kv) (snd kv) nr).
proof: Proof. unfold EnsembleReplace, EnsembleRemove, EnsembleFMapEquivalence; intros; intuition. destruct (string_dec k (fst kv)); subst. left. rewrite (StringIndexedMap.find_1 (StringIndexedMap.add_1 nr (snd kv) (refl_equal (fst kv)))) in *; destruct kv; simpl in *; f_equal; congruence. right; split; eauto. eapply H. eauto using StringIndexedMap.find_1, StringIndexedMap.add_3, StringIndexedMap.find_2. subst; simpl in *. eauto using StringIndexedMap.find_1, StringIndexedMap.add_1. destruct (string_dec k (fst kv)); subst. simpl in H1; congruence. destruct (H k). generalize (H4 _ H3). eauto using StringIndexedMap.find_1, StringIndexedMap.add_2, StringIndexedMap.find_2. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.Strings.String Coq.ZArith.ZArith Coq.Lists.List Coq.Logic.FunctionalExtensionality Coq.Sets.Ensembles Computation ADT ADTRefinement ADTNotation BuildADTRefinements KVEnsembles String_as_OT FMapAVL