proposition: Lemma is_sub_domain_equal_maps {elt elt2} : forall m1 m2 m1' m2', M.Equal (elt := elt) m1 m1' -> M.Equal (elt := elt2) m2 m2' -> is_sub_domain m1 m2 = is_sub_domain m1' m2'.
proof: Proof. unfold is_sub_domain. unfold UWFacts.WFacts.keys. intros. case_eq (forallb (fun k : M.key => M.mem (elt:=elt2) k m2) (map fst (M.elements (elt:=elt) m1))). intros. rewrite forallb_forall in H1. repeat rewrite (proj2 (forallb_forall _ _) ); eauto; intros. rewrite <- H0; apply H1. apply In_fst_elements_In; apply In_fst_elements_In in H2. rewrite H; eauto. intros. rewrite forallb_forall_false in H1. rewrite (proj2 (forallb_forall_false _ _) ); eauto. intro; apply H1; intros. rewrite H0; apply H2. apply In_fst_elements_In; apply In_fst_elements_In in H3. rewrite <- H; 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