proposition: Lemma length_AxiomatizeMethodPre' av dom domWrap : forall l l' l'', AxiomatizeMethodPre' (av := av) l'' dom domWrap l' l -> Datatypes.length l' + Datatypes.length l'' + Datatypes.length dom = Datatypes.length l.
proof: Proof. induction dom; simpl in *; intros; subst. - rewrite app_length; eauto. - destruct H. eapply IHdom in H; simpl in H. rewrite <- H; omega. 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