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