Resolve issues related to the update (mem got swapped + ignore unused…

… variables)

Minimal/ARS.lean

@@ -159,6 +159,7 @@ theorem decr {a b c} (ab : r a b) (b_c : ReflTransGen r b c)
   | .head _ _ => by
       simp [ReflTransGen.size]
 
+set_option linter.unusedVariables false
 def z_confluence
   (z : ZProperty r)
   {a b c : α}
@@ -187,3 +188,4 @@ def z_implies_confluence
   (z : ZProperty r)
   : Confluence r
   := λ _ _ _ ab ac => z_confluence z ab ac
+set_option linter.unusedVariables true

Minimal/Record.lean

@@ -15,22 +15,22 @@ inductive Record (α : Type u) : List String → Type u where
     → Record α (key :: keys)
 
 -- value ∈ record
-inductive Mem : {keys : List String} → (a : α) → Record α keys → Prop where
+inductive Mem : {keys : List String} → Record α keys → (a : α) → Prop where
   | head
     : {keys : List String}
     → {a : α}
     → {as : Record α keys}
     → (key : String)
     → (not_in : key ∉ keys)
-    → Mem a (Record.cons key not_in a as)
+    → Mem (Record.cons key not_in a as) a
   | tail
     : {keys : List String}
     → {a b : α}
     → {as : Record α keys}
     → (key : String)
     → (not_in : key ∉ keys)
-    → Mem a as
-    → Mem a (Record.cons key not_in b as)
+    → Mem as a
+    → Mem (Record.cons key not_in b as) a
 
 instance {keys : List String} : Membership α (Record α keys) where
   mem := Mem

Minimal/Utils.lean

@@ -6,5 +6,5 @@ theorem notEqByListMem
   : a ≠ b
   := λ eq =>
     let memEq : List.Mem a lst = List.Mem b lst :=
-      congrArg (λ x => Membership.mem x lst) eq
+      congrArg (λ x => Membership.mem lst x) eq
     b_not_in (Eq.mp memEq a_is_in)