proposition: Lemma hlist_app_hlist_split : forall ls' ls (h : hlist (ls ++ ls')), hlist_app (fst (hlist_split ls ls' h)) (snd (hlist_split ls ls' h)) = h.
proof: Proof. induction ls; simpl; intros; auto. rewrite (hlist_eta h); simpl. specialize (IHls (hlist_tl h)). destruct (hlist_split ls ls' (hlist_tl h)); simpl in *; auto. 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