proposition: Lemma hlist_map_ext : forall (ff gg : forall x, F x -> G x), (forall x t, ff x t = gg x t) -> forall ls (hl : hlist F ls), hlist_map ff hl = hlist_map gg hl.
proof: Proof. induction hl; simpl; auto. intros. f_equal; auto. Defined.
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