fix: List.Mem should have two parameters

src/Init/Data/List/Basic.lean

@@ -240,9 +240,9 @@ def notElem [BEq α] (a : α) (as : List α) : Bool :=
 abbrev contains [BEq α] (as : List α) (a : α) : Bool :=
   elem a as
 
-inductive Mem : α → List α → Prop
-  | head (a : α) (as : List α) : Mem a (a::as)
-  | tail (a : α) {b : α} {as : List α} : Mem b as → Mem b (a::as)
+inductive Mem (a : α) : List α → Prop
+  | head (as : List α) : Mem a (a::as)
+  | tail (b : α) {as : List α} : Mem a as → Mem a (b::as)
 
 instance : Membership α (List α) where
   mem := Mem

tests/lean/run/dotNameIssue.lean

@@ -1,7 +1,7 @@
 example : x ≠ y → x ∉ [y] :=
   fun hne hin =>
     match hin with
-    | .head _ _ => hne rfl
+    | .head _ => hne rfl
 
 example : x ≠ y → x ∉ [y] :=
-  fun hne (.head _ _) => hne rfl
+  fun hne (.head _) => hne rfl