fact: Definition get_next ls y x (m : member x (y :: ls)) : option (member x ls) := match m in member _ ls' return match ls' with | nil => unit | l' :: ls' => option (member x ls') end with | MZ _ => None | MN _ _ m => Some m end.
imports: Coq.Lists.List Relations RelationClasses ExtLib.Core.RelDec ExtLib.Data.SigT ExtLib.Data.ListNth ExtLib.Data.Option ExtLib.Tactics.Injection ExtLib.Tactics.EqDep