michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

fix(library/standard): congr1 and congr2 theorem definition, we should allow A and B to inhabit different universes

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-07-03 16:25:14 -07:00
parent 7d27368708
commit 9ec4f23522
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
library/standard/logic.lean
View file

@ -92,10 +92,10 @@ theorem symm {A : Type} {a b : A} (H : a = b) : b = 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
theorem congr2 {A : Type} {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
theorem congr {A : Type} {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