fact: Definition CompileUnit2Equiv av env {A} {n n'} {consSigs : Vector.t consSig n} {methSigs : Vector.t methSig n'} (adt : DecoratedADT (BuildADTSig consSigs methSigs)) RepInv (f : A -> _) g ax_mod_name' op_mod_name' cWrap dWrap rWrap {exports} (compileUnit : CompileUnit exports) := DFModuleEquiv (av := av) env adt RepInv compileUnit.(module) cWrap dWrap (f rWrap) g /\ compileUnit.(ax_mod_name) = ax_mod_name' /\ compileUnit.(op_mod_name) = op_mod_name'.
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