lean2/tests/lean/run/elim2.lean
Leonardo de Moura cbc81ea6c5 chore(*): minimize dependencies on tests
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-24 19:58:48 -07:00

8 lines
268 B
Text

import logic
using num tactic
variable p : num → num → num → Prop
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
:= obtain a b c H [fact], from H1,
by (apply exists_intro; apply H2; eassumption)