fact: Fixpoint to_nat {ls} (m : member a ls) : nat := match m with | MZ _ => 0 | MN _ _ m => S (to_nat 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