fact: Fixpoint cMethodType' (rep : Type) (dom : list Type) (cod : option Type) : Type := match dom with | nil => match cod with | Some cod' => (prod rep cod') | None => rep end | cons d dom' => d -> cMethodType' rep dom' cod end.
imports: Fiat.Common Fiat.Computation Fiat.ADT.ADTSig Fiat.ADT Coq.Sets.Ensembles