fact: Fixpoint methodType' (rep : Type) (dom : list Type) (cod : option Type) : Type := match dom with | nil => match cod with | Some cod' => Comp (rep * cod') | _ => Comp rep end | cons d dom' => d -> methodType' rep dom' cod end.
imports: Fiat.Common Fiat.Computation