proposition: Lemma is_sub_domain_add {elt elt2} : forall k (v : elt) (v' : elt2) m1 m2, ~ StringMap.In k m1 -> ~ StringMap.In k m2 -> is_sub_domain ([k |> v] :: m1) ([k |> v'] :: m2) = is_sub_domain m1 m2.
proof: Proof. intros; unfold is_sub_domain. case_eq (forallb (fun k0 : M.key => M.mem (elt:=elt2) k0 ([k |> v']::m2)) (UWFacts.WFacts.keys ([k |> v]::m1))); intros. - rewrite forallb_forall in H1. symmetry; apply forallb_forall; intros. erewrite <- add_neq_b. apply H1. apply In_fst_elements_In. apply add_in_iff; right. apply In_fst_elements_In; apply H2. intro; subst. apply H. apply In_fst_elements_In; apply H2. - rewrite forallb_forall_false in H1. symmetry; apply forallb_forall_false. intro; apply H1; intros. unfold UWFacts.WFacts.keys in H3. rewrite In_fst_elements_In in H3. apply mem_in_iff; apply add_in_iff. apply add_in_iff in H3; intuition subst. rewrite <- In_fst_elements_In in H4. apply H2 in H4; right. apply mem_in_iff; eauto. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Fiat.ADT.Core Bedrock.Platform.Facade.DFModule Fiat.ADTNotation Bedrock.Platform.Facade.CompileUnit2 Fiat.Common.i3list Fiat.Common.ilist3 CertifiedExtraction.Core CertifiedExtraction.FacadeUtils CertifiedExtraction.StringMapUtils CertifiedExtraction.Extraction.Internal CertifiedExtraction.Extraction.Extraction