test-suite/success/Discriminate.v


1
2
3
4
5
6
7
8
9
10
11

(* Check the behaviour of Discriminate *)

(* Check that Discriminate tries Intro until *)

Lemma l1 : O=(S O)->False.   
Discriminate 1.
Qed.

Lemma l2 : (H:O=(S O))H==H.   
Discriminate H.
Qed.