proposition: Lemma member_In : forall ls (t : T), member t ls -> List.In t ls.
proof: Proof. induction 1; simpl; 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