proposition: Theorem nth_error_get_hlist_nth_Some : forall ls n s, nth_error_get_hlist_nth ls n = Some s -> exists pf : nth_error ls n = Some (projT1 s), forall h, projT2 s h = match pf in _ = t return match t return Type with | Some t => F t | None => unit end with | eq_refl => hlist_nth h n end.
proof: Proof. induction ls; simpl; intros; try congruence. { destruct n. { inv_all; subst; simpl. exists (eq_refl). intros. rewrite (hlist_eta h). reflexivity. } { forward. inv_all; subst. destruct (IHls _ _ H0); clear IHls. simpl in *. exists x0. intros. rewrite (hlist_eta h). 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