proposition: Lemma hlist_gen_member_hlist_map : forall A (F G : A -> Type) (ff : forall t, F t -> G t) ls f, hlist_map ff (hlist_gen_member F (ls := ls) f) = hlist_gen_member G (fun a M => ff _ (f _ M)).
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