fact: Fixpoint wrap (ls : list Type) R {struct ls} : (tuple ls -> R) -> ftype ls R := match ls as ls return (tuple ls -> R) -> ftype ls R with | nil => fun f => f tt | cons l ls => fun f => fun x => wrap ls (fun g => f (x,g)) end.
imports: ExtLib.Structures.Monad