proposition: Lemma hlist_gen_ext : forall A F (f g : forall a, F a), (forall x, f x = g x) -> forall ls : list A, hlist_gen f ls = hlist_gen g ls.
proof: Proof. intros. do 2 rewrite <- hlist_gen_member_hlist_gen. apply hlist_gen_member_ext. 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