From df8ebeeefcea61b498c83c06c49df0ed2f29acb4 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 16 Apr 2015 14:04:09 -0700 Subject: [PATCH] feat(library/logic/axioms/examples/diaconescu): remove redundant hypothesis --- library/logic/axioms/examples/diaconescu.lean | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/library/logic/axioms/examples/diaconescu.lean b/library/logic/axioms/examples/diaconescu.lean index 5be766237..9f108543c 100644 --- a/library/logic/axioms/examples/diaconescu.lean +++ b/library/logic/axioms/examples/diaconescu.lean @@ -9,7 +9,6 @@ open eq.ops nonempty inhabited -- Show that Excluded middle follows from -- Hilbert's choice operator, function extensionality and Prop extensionality context -hypothesis propext {a b : Prop} : (a → b) → (b → a) → a = b parameter p : Prop private definition u [reducible] := epsilon (λx, x = true ∨ p) @@ -40,7 +39,7 @@ assume Hp : p, have Hr : (x = false ∨ p) → (x = true ∨ p), from assume A, or.inr Hp, show (x = true ∨ p) = (x = false ∨ p), from - propext Hl Hr), + propext (iff.intro Hl Hr)), show u = v, from Hpred ▸ (eq.refl (epsilon (λ x, x = true ∨ p)))