proposition: Theorem hlist_app_hlist_map : forall ls ls' (a : hlist F ls) (b : hlist F ls'), hlist_map (hlist_app a b) = hlist_app (hlist_map a) (hlist_map b).
proof: Proof. induction a. simpl; auto. simpl. intros. 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