fact: Fixpoint hlist_gen_member ls : (forall a, member a ls -> F a) -> hlist F ls := match ls as ls return ((forall a : A, member a ls -> F a) -> hlist F ls) with | nil => fun _ => Hnil | a :: ls' => fun fm => Hcons (fm a (MZ a ls')) (hlist_gen_member (fun a' (M : member a' ls') => fm a' (MN a M))) end.
imports: Coq.Lists.List Coq.Arith.PeanoNat Relations RelationClasses ExtLib.Core.RelDec ExtLib.Data.SigT ExtLib.Data.Member ExtLib.Data.ListNth ExtLib.Data.Option ExtLib.Tactics Coq.Classes.Morphisms