From 2ea1e68f25ca92a12227919485eee47c73d3716b Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 30 Jun 2014 12:00:47 -0700 Subject: [PATCH] feat(library/standard): add equal_f theorem Signed-off-by: Leonardo de Moura --- library/standard/logic.lean | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/library/standard/logic.lean b/library/standard/logic.lean index d4fa94a88c..7256eb8824 100644 --- a/library/standard/logic.lean +++ b/library/standard/logic.lean @@ -73,12 +73,15 @@ theorem trans {A : Type} {a b c : A} (H1 : a = b) (H2 : b = c) : a = c theorem symm {A : Type} {a b : A} (H : a = b) : b = a := subst H (refl a) -theorem congr1 {A B : Type} {f g : A → B} (H : f = g) (a : A) : f a = g a +theorem congr1 {A : Type} {B : A → Type} {f g : Π x, B x} (H : f = g) (a : A) : f a = g a := subst H (refl (f a)) theorem congr2 {A B : Type} {a b : A} (f : A → B) (H : a = b) : f a = f b := subst H (refl (f a)) +theorem equal_f {A : Type} {B : A → Type} {f g : Π x, B x} (H : f = g) : ∀ x, f x = g x +:= take x, congr1 H x + definition cast {A B : Type} (H : A = B) (a : A) : B := eq_rec a H