proposition: Lemma hlist_split_hlist_app : forall ls' ls (h : hlist ls) (h' : hlist ls'), hlist_split _ _ (hlist_app h h') = (h,h').
proof: Proof. induction ls; simpl; intros. { rewrite (hlist_eta h); simpl; auto. } { rewrite (hlist_eta h); simpl. rewrite IHls. reflexivity. } 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