2014-01-29 22:21:18 +00:00
|
|
|
import tactic
|
|
|
|
|
variable f {A : TypeU} : A → A
|
|
|
|
|
axiom Ax1 (a : Bool) : f a = not a
|
|
|
|
|
axiom Ax2 (a : Nat) : f a = 0
|
|
|
|
|
rewrite_set S
|
2014-02-02 02:27:14 +00:00
|
|
|
add_rewrite Ax1 Ax2 not_false : S
|
2014-01-29 22:21:18 +00:00
|
|
|
theorem T1 (a : Nat) : f (f a > 0)
|
|
|
|
|
:= by simp S
|
|
|
|
|
print environment 1
|
