From d77bdaabc26b14fe39896a90e5533728e2a5394e Mon Sep 17 00:00:00 2001 From: Jeremy Avigad Date: Sun, 9 Aug 2015 21:31:17 -0400 Subject: [PATCH] refactor(library/logic/eq): rename two theorems --- library/logic/eq.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/library/logic/eq.lean b/library/logic/eq.lean index 155858bc1..4ba2b3e78 100644 --- a/library/logic/eq.lean +++ b/library/logic/eq.lean @@ -106,12 +106,12 @@ end section variables {p : Prop} - theorem p_ne_false : p → p ≠ false := + theorem ne_false_of_self : p → p ≠ false := assume (Hp : p) (Heq : p = false), Heq ▸ Hp - theorem p_ne_true : ¬p → p ≠ true := + theorem ne_true_of_not : ¬p → p ≠ true := assume (Hnp : ¬p) (Heq : p = true), (Heq ▸ Hnp) trivial end theorem true_ne_false : ¬true = false := -p_ne_false trivial +ne_false_of_self trivial