fact: Definition BuildCompileUnit2TSpec av (env : Env av) {A} {n n'} {consSigs : Vector.t consSig n} {methSigs : Vector.t methSig n'} (adtSpec : DecoratedADT (BuildADTSig consSigs methSigs)) (adtImpl : DecoratedADT (BuildADTSig consSigs methSigs)) (AbsR : Core.Rep adtSpec -> Core.Rep adtImpl -> Prop) RepInv numRepArgs (DecomposeRep : A -> _) DecomposeRepPre DecomposeRepPost g ax_mod_name' op_mod_name' cWrap dWrap rWrap H ValidImpl (exports := GenExports (numRepArgs := numRepArgs) cWrap dWrap AbsR RepInv DecomposeRepPre DecomposeRepPost H ValidImpl) := {compileUnit : CompileUnit exports & (CompileUnit2Equiv env adtImpl RepInv DecomposeRep g ax_mod_name' op_mod_name' cWrap dWrap rWrap compileUnit) }.
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