fact: Record GoodWrapper av A := { gWrap : FacadeWrapper (Value av) A; gWrapTag : bool; gWrapTagConsistent : if gWrapTag then forall a : A, exists adt, wrap a = ADT adt else forall a : A, exists w, wrap a = SCA _ w }.
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