proposition: Theorem hlist_map_hlist_map : forall ls (hl : hlist F ls), hlist_map gg (hlist_map ff hl) = hlist_map (fun _ x => gg (ff x)) hl.
proof: Proof. induction hl; simpl; f_equal. assumption. 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