proposition: Lemma member_case : forall x ls (m : member x ls), match ls as ls return member x ls -> Prop with | nil => fun _ => False | l :: ls' => fun m => (exists (pf : l = x), m = match pf in _ = z return member z (l :: ls') with | eq_refl => MZ _ ls' end) \/ exists m' : member x ls', m = MN _ m' end m.
proof: Proof. induction m. { left. exists eq_refl. reflexivity. } { right. eauto. } 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