2013-12-05 03:22:12 -08:00
|
|
|
|
Set: pp::colors
|
|
|
|
|
Set: pp::unicode
|
2013-12-30 13:35:37 -08:00
|
|
|
|
Imported 'tactic'
|
2014-01-01 13:52:25 -08:00
|
|
|
|
Imported 'Int'
|
2013-12-05 03:22:12 -08:00
|
|
|
|
Assumed: f
|
|
|
|
|
Assumed: P
|
|
|
|
|
Assumed: Ax1
|
|
|
|
|
Proved: T1
|
|
|
|
|
Assumed: b
|
|
|
|
|
Assumed: Ax2
|
|
|
|
|
Proved: T2
|
2013-12-26 15:54:53 -08:00
|
|
|
|
Proved: T3
|
2014-01-05 19:10:21 -08:00
|
|
|
|
theorem T2 (a : ℤ) : P a a ⇒ f a a := discharge (λ H : P a a, Ax1 a a H)
|
|
|
|
|
theorem T3 (a : ℤ) : P a a ⇒ f a a := discharge (λ H : P a a, Ax1 a a H)
|