fact: Fixpoint nth_error_hlist_nth ls (n : nat) : option (hlist ls -> match nth_error ls n with | None => Empty_set | Some x => F x end) := match ls as ls return option (hlist ls -> match nth_error ls n with | None => Empty_set | Some x => F x end) with | nil => None | l :: ls => match n as n return option (hlist (l :: ls) -> match nth_error (l :: ls) n with | None => Empty_set | Some x => F x end) with | 0 => Some hlist_hd | S n => match nth_error_hlist_nth ls n with | None => None | Some f => Some (fun h => f (hlist_tl h)) end 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