fact: Fixpoint hlist_to_tuple ps (h : hlist (fun x : Type => x) ps) : asTuple ps := match h in hlist _ ps return asTuple ps with | Hnil => tt | Hcons x h => (x,hlist_to_tuple h) end.
imports: Coq.Lists.List ExtLib.Data.Member ExtLib.Data.HList ExtLib.Generic.Func