proposition: Lemma nth_error_get_hlist_nth_weaken : forall ls ls' n x, nth_error_get_hlist_nth ls n = Some x -> exists z, nth_error_get_hlist_nth (ls ++ ls') n = Some (@existT iT (fun t => hlist (ls ++ ls') -> F t) (projT1 x) z) /\ forall h h', projT2 x h = z (hlist_app h h').
proof: Proof. intros ls ls'. revert ls. induction ls; simpl; intros; try congruence. { destruct n; inv_all; subst. { simpl. eexists; split; eauto. intros. rewrite (hlist_eta h). reflexivity. } { forward. inv_all; subst. simpl. apply IHls in H0. forward_reason. rewrite H. eexists; split; eauto. intros. rewrite (hlist_eta h). simpl in *. 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