fact: Definition AxiomatizeMethodPreSpec (av : Type) {RepImpl RepSpec} {Dom} {numRepArgs : nat} (AbsR : RepSpec -> RepImpl -> Prop) (P : RepImpl -> Prop) (f : RepImpl -> Vector.t (Value av) numRepArgs) : DomWrapperT av Dom -> list (Value av) -> Prop := fun dWrap args => exists r r', AbsR r r' /\ P r' /\ AxiomatizeMethodPre' (Vector.to_list (f r')) Dom dWrap [] args.
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