diff options
Diffstat (limited to 'tests/example2.v')
| -rw-r--r-- | tests/example2.v | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/tests/example2.v b/tests/example2.v index 398f33561e..ca9e3dcff5 100644 --- a/tests/example2.v +++ b/tests/example2.v @@ -19,3 +19,10 @@ Proof. let myvar := Std.NamedHyp @x in split with (?myvar := 0). split. Qed. + +Goal (forall n : nat, n = 0 -> False) -> True. +Proof. +intros H. +elim &H with 0. +split. +Qed. |