2014-08-24 19:58:48 -07:00
|
|
|
import logic
|
2014-09-03 16:00:38 -07:00
|
|
|
open num tactic
|
2014-07-22 09:43:18 -07:00
|
|
|
variable p : num → num → num → Prop
|
2014-07-11 04:51:28 +01:00
|
|
|
axiom H1 : ∃ x y z, p x y z
|
|
|
|
|
axiom H2 : ∀ {x y z : num}, p x y z → p x x x
|
|
|
|
|
theorem tst : ∃ x, p x x x
|
2014-07-12 06:35:24 +01:00
|
|
|
:= obtain a b c H [fact], from H1,
|
2014-07-11 04:51:28 +01:00
|
|
|
by (apply exists_intro; apply H2; eassumption)
|
