fact: Fixpoint applyRest (f : list {x : Type & T -> x}) : Ctor f -> T := match f as f return Ctor f -> T with | nil => fun x => x | a :: b => fun acc => applyRest b (acc ((projT2 a) rec)) end.
imports: Coq.Lists.List