proposition: Lemma nth_error_get_hlist_nth_appL : forall tvs' tvs n, n < length tvs -> exists x, nth_error_get_hlist_nth (tvs ++ tvs') n = Some x /\ exists y, nth_error_get_hlist_nth tvs n = Some (@existT _ _ (projT1 x) y) /\ forall vs vs', (projT2 x) (hlist_app vs vs') = y vs.
proof: Proof. clear. induction tvs; simpl; intros. { exfalso; inversion H. } { destruct n. { clear H IHtvs. eexists; split; eauto. eexists; split; eauto. simpl. intros. rewrite (hlist_eta vs). reflexivity. } { apply Nat.succ_lt_mono in H. { specialize (IHtvs _ H). forward_reason. rewrite H0. rewrite H1. forward. subst. simpl in *. eexists; split; eauto. eexists; split; eauto. simpl. intros. rewrite (hlist_eta vs). simpl. 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