From b4d765ff2e8092ffdea047de4404f5146cc031b1 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 9 Sep 2014 19:11:03 -0700 Subject: [PATCH] refactor(library/logic/core/cast): cleanup --- library/logic/core/cast.lean | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/library/logic/core/cast.lean b/library/logic/core/cast.lean index d08c87cfc3..4c8c76141c 100644 --- a/library/logic/core/cast.lean +++ b/library/logic/core/cast.lean @@ -12,14 +12,14 @@ definition cast {A B : Type} (H : A = B) (a : A) : B := eq.rec a H theorem cast_refl {A : Type} (a : A) : cast (eq.refl A) a = a := -eq.refl (cast (eq.refl A) a) +rfl theorem cast_proof_irrel {A B : Type} (H1 H2 : A = B) (a : A) : cast H1 a = cast H2 a := -eq.refl (cast H1 a) +rfl theorem cast_eq {A : Type} (H : A = A) (a : A) : cast H a = a := -calc cast H a = cast (eq.refl A) a : cast_proof_irrel H (eq.refl A) a - ... = a : cast_refl a +calc cast H a = cast (eq.refl A) a : rfl + ... = a : rfl definition heq {A B : Type} (a : A) (b : B) := ∃H, cast H a = b