fact: Fixpoint AxiomatizeMethodPre' (av : Type) (RepArgs : list (Value av)) {Dom} {struct Dom} : DomWrapperT av Dom -> list (Value av) -> list (Value av) -> Prop := match Dom return DomWrapperT av Dom -> list (Value av) -> list (Value av) -> Prop with | nil => fun dWrap args' args => app args' RepArgs = args | cons DomT Dom' => fun dWrap args' args => let wrap' := gWrap (fst dWrap) in exists x : DomT, AxiomatizeMethodPre' RepArgs Dom' (snd dWrap) (wrap x :: args') args end.
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