From 9ebcd9c2ffe2c27da61bccec73076115c7a9475b Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 2 Aug 2016 15:53:35 -0700 Subject: [PATCH] fix(library/init/sigma_lex): closes #1091 --- library/init/sigma_lex.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/library/init/sigma_lex.lean b/library/init/sigma_lex.lean index a59c823ea6..1bdae16398 100644 --- a/library/init/sigma_lex.lean +++ b/library/init/sigma_lex.lean @@ -14,8 +14,8 @@ section -- Lexicographical order based on Ra and Rb inductive lex : sigma B → sigma B → Prop := - | left : ∀{a₁ b₁} a₂ b₂, Ra a₁ a₂ → lex ⟨a₁, b₁⟩ ⟨a₂, b₂⟩ - | right : ∀a {b₁ b₂}, Rb a b₁ b₂ → lex ⟨a, b₁⟩ ⟨a, b₂⟩ + | left : ∀ {a₁ : A} (b₁ : B a₁) {a₂ : A} (b₂ : B a₂), Ra a₁ a₂ → lex ⟨a₁, b₁⟩ ⟨a₂, b₂⟩ + | right : ∀ (a : A) {b₁ b₂ : B a}, Rb a b₁ b₂ → lex ⟨a, b₁⟩ ⟨a, b₂⟩ end