aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/success/Simplify_eq.v
blob: 5b856e3da0ebbb9c15c4ca5c3f206a3820f6d1ee (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
(* Check the behaviour of Simplify_eq *)

(* Check that Simplify_eq tries Intro until *)

Lemma l1 : 0 = 1 -> False.   
 simplify_eq 1.
Qed.

Lemma l2 : forall (x : nat) (H : S x = S (S x)), H = H -> False.   
 simplify_eq H.
intros.
apply (n_Sn x H0).
Qed.