fact: Definition HideADT (extADT : ADT extSig) : ADT resSig := match extADT with {| Rep := rep; Constructors := extConstructors; Methods := extMethods |} => Build_ADT resSig (fun idx => extConstructors (constructorMap idx)) (fun idx => extMethods (methodMap idx)) end.
imports: Fiat.Common Fiat.Computation.Core Fiat.ADT.Core Coq.Sets.Ensembles