proposition: Theorem nth_error_get_hlist_nth_None : forall ls n, nth_error_get_hlist_nth ls n = None <-> nth_error ls n = None.
proof: Proof. induction ls; simpl; intros; try congruence. { destruct n; intuition. } { destruct n; simpl; try solve [ intuition congruence ]. specialize (IHls n). forward. } 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