proposition: Theorem hlist_get_hlist_map : forall ls t (hl : hlist F ls) (m : member t ls), hlist_get m (hlist_map ff hl) = ff (hlist_get m hl).
proof: Proof. induction m; simpl. { rewrite (hlist_eta hl). reflexivity. } { rewrite (hlist_eta hl). simpl. 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