proposition: Lemma member_eta : forall x ls (m : member x ls), m = match m in member _ ls return member x ls with | MZ ls => MZ x ls | MN _ _ n => MN _ n end.
proof: Proof. destruct m; auto. Qed.
imports: Coq.Lists.List Relations RelationClasses ExtLib.Core.RelDec ExtLib.Data.SigT ExtLib.Data.ListNth ExtLib.Data.Option ExtLib.Tactics.Injection ExtLib.Tactics.EqDep