fact: Record ADTSig := { ConstructorIndex : Type; MethodIndex : Type; ConstructorDom : ConstructorIndex -> list Type; MethodDomCod : MethodIndex -> (list Type) * (option Type) }.
imports: Fiat.Common Fiat.Computation