fact: Fixpoint uncurry {D R} {struct D} : (asTuple D -> R) -> asFunc D R := match D as D return (asTuple D -> R) -> asFunc D R with | nil => fun x => x tt | d :: D => fun f d => uncurry (fun x => f (d, x)) end.
imports: Coq.Lists.List ExtLib.Data.Member