proposition: Lemma AbsR_add_EnsembleInsert {A} : forall nr kv or, EnsembleFMapEquivalence or nr -> StringIndexedMap.find (elt:=A) (fst kv) nr = None -> EnsembleFMapEquivalence (fun kv' => kv' = kv \/ or kv') (StringIndexedMap.add (fst kv) (snd kv) nr).
proof: Proof. unfold SubEnsembleInsert, 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. pose proof (H k); intuition. 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. apply H in H2. rewrite H0 in H2; discriminate. apply H in H2. 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 CacheSpec CacheRefinements String_as_OT FMapAVL