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