fact: Record ADT (Sig : ADTSig) := { Rep : Type; Constructors : forall idx : ConstructorIndex Sig, constructorType Rep (ConstructorDom Sig idx); Methods : forall idx : MethodIndex Sig, methodType Rep (fst (MethodDomCod Sig idx)) (snd (MethodDomCod Sig idx)) }.
imports: Fiat.Common Fiat.Computation Fiat.ADT.ADTSig Coq.Sets.Ensembles