diff --git a/tests/lean/param_binder_update2.lean b/tests/lean/param_binder_update2.lean
new file mode 100644
index 000000000..862c293e9
--- /dev/null
+++ b/tests/lean/param_binder_update2.lean
@@ -0,0 +1,23 @@
+section
+  parameters {A : Type} {B : Type}
+
+  definition foo1 (a : A) (b : B) := a
+
+  parameters (B) {A} -- Should not change the order of the parameters
+
+  definition foo2 (a : A) (b : B) := a
+
+  parameters {B} (A)
+
+  definition foo3 (a : A) (b : B) := a
+
+  parameters (A) (B)
+
+  definition foo4 (a : A) (b : B) := a
+
+end
+
+check @foo1
+check @foo2
+check @foo3
+check @foo4
diff --git a/tests/lean/param_binder_update2.lean.expected.out b/tests/lean/param_binder_update2.lean.expected.out
new file mode 100644
index 000000000..b5b750ee7
--- /dev/null
+++ b/tests/lean/param_binder_update2.lean.expected.out
@@ -0,0 +1,4 @@
+foo1 : Π {A : Type} {B : Type}, A → B → A
+foo2 : Π {A : Type} (B : Type), A → B → A
+foo3 : Π (A : Type) {B : Type}, A → B → A
+foo4 : Π (A : Type) (B : Type), A → B → A