From 528d51bc57d0a9037f6f9fe49bbd66ff7be39d2c Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 3 Jul 2014 09:44:36 -0700 Subject: [PATCH] feat(library/standard): add congr theorem Signed-off-by: Leonardo de Moura --- library/standard/logic.lean | 3 +++ 1 file changed, 3 insertions(+) diff --git a/library/standard/logic.lean b/library/standard/logic.lean index ce52928f4..bbce237d2 100644 --- a/library/standard/logic.lean +++ b/library/standard/logic.lean @@ -95,6 +95,9 @@ theorem congr1 {A : Type} {B : A → Type} {f g : Π x, B x} (H : f = g) (a : 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 congr {A B : Type} {f g : A → B} {a b : A} (H1 : f = g) (H2 : a = b) : f a = g b +:= subst H1 (subst H2 (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