2015-12-06 02:17:15 +00:00
|
|
|
set_option blast.strategy "preprocess"
|
2015-11-13 23:27:54 +00:00
|
|
|
|
|
|
|
|
example (a b : nat) : a = b → b = a :=
|
|
|
|
|
by blast
|
|
|
|
|
|
|
|
|
|
example (a b c : nat) : a = b → a = c → b = c :=
|
|
|
|
|
by blast
|
|
|
|
|
|
|
|
|
|
example (p : nat → Prop) (a b c : nat) : a = b → a = c → p b → p c :=
|
|
|
|
|
by blast
|
