2013-12-07 15:37:54 -08:00
|
|
|
|
Set: pp::colors
|
|
|
|
|
Set: pp::unicode
|
2014-01-01 13:52:25 -08:00
|
|
|
|
Imported 'Int'
|
2013-12-07 15:37:54 -08:00
|
|
|
|
Proved: T1
|
2014-01-05 12:05:08 -08:00
|
|
|
|
theorem T1 (a b : ℤ) (f : ℤ → ℤ) (assumption : a = b) : f (f a) = f (f b) :=
|
2014-01-05 19:10:21 -08:00
|
|
|
|
congr (refl f) (congr (refl f) assumption)
|