fact: Fixpoint hlist_nth_error {ls} (hs : hlist ls) (n : nat) : option (match nth_error ls n with | None => unit | Some x => F x end) := match hs in hlist ls return option (match nth_error ls n with | None => unit | Some x => F x end) with | Hnil => None | Hcons l ls h hs => match n as n return option (match nth_error (l :: ls) n with | None => unit | Some x => F x end) with | 0 => Some h | S n => hlist_nth_error hs n end end.
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