proposition: Lemma hlist_tl_snd_hlist_split : forall t (xs ys : list _) (h : hlist (t :: xs ++ ys)), snd (hlist_split xs ys (hlist_tl h)) = snd (hlist_split (t :: xs) ys h).
proof: Proof. simpl. intros. match goal with | |- context [ match ?X with _ => _ end ] => remember X end. destruct p. simpl. change h1 with (snd (h0, h1)). rewrite Heqp. 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