2015-11-14 23:02:14 +00:00
|
|
|
import data.list
|
|
|
|
|
|
2015-12-07 19:59:21 +00:00
|
|
|
set_option blast.strategy "unit"
|
2015-11-14 23:02:14 +00:00
|
|
|
|
|
|
|
|
definition lemma1 : true :=
|
|
|
|
|
by blast
|
|
|
|
|
|
|
|
|
|
open perm
|
|
|
|
|
|
|
|
|
|
definition lemma2 (l : list nat) : l ~ l :=
|
|
|
|
|
by blast
|
|
|
|
|
|
|
|
|
|
print lemma1
|
|
|
|
|
print lemma2
|
