diff --git a/library/init/wf.lean b/library/init/wf.lean
index 13994eee69..547a202f10 100644
--- a/library/init/wf.lean
+++ b/library/init/wf.lean
@@ -153,8 +153,8 @@ section
 
   -- Lexicographical order based on ra and rb
   inductive lex : α × β → α × β → Prop
-  | left  : ∀ {a₁ b₁} a₂ b₂, ra a₁ a₂ → lex (a₁, b₁) (a₂, b₂)
-  | right : ∀ a {b₁ b₂},     rb b₁ b₂ → lex (a, b₁)  (a, b₂)
+  | left  : ∀ {a₁} b₁ {a₂} b₂, ra a₁ a₂ → lex (a₁, b₁) (a₂, b₂)
+  | right : ∀ a {b₁ b₂},       rb b₁ b₂ → lex (a, b₁)  (a, b₂)
 
   -- relational product based on ra and rb
   inductive rprod : α × β → α × β → Prop
@@ -183,7 +183,7 @@ section
 
   -- relational product is a subrelation of the lex
   def rprod_sub_lex : ∀ a b, rprod ra rb a b → lex ra rb a b :=
-  λ a b h, prod.rprod.rec_on h (λ a₁ b₁ a₂ b₂ h₁ h₂, lex.left rb a₂ b₂ h₁)
+  λ a b h, prod.rprod.rec_on h (λ a₁ b₁ a₂ b₂ h₁ h₂, lex.left rb b₁ b₂ h₁)
 
   -- The relational product of well founded relations is well-founded
   def rprod_wf (ha : well_founded ra) (hb : well_founded rb) : well_founded (rprod ra rb) :=