fact: Definition cConstructors {Sig : ADTSig} (c : cADT Sig) (idx : ConstructorIndex Sig) : cConstructorType (cRep c) (ConstructorDom Sig idx) := pcConstructors (projT2 c) idx.
imports: Fiat.Common Fiat.Computation Fiat.ADT.ADTSig Fiat.ADT Coq.Sets.Ensembles