proposition: Lemma hlist_gen_member_ext : forall ls (f g : forall a, member a ls -> F a), (forall x M, f x M = g x M) -> hlist_gen_member f = hlist_gen_member g.
proof: Proof. intros. induction ls; simpl; f_equal; auto. Qed.
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