blob: f3f2195228b1b27eab24546c10ceff27edc0db5d (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
|
Require Export Coq.Classes.RelationClasses.
Section defs.
Variable A : Type.
Variable lt : A -> A -> Prop.
Context {ltso : StrictOrder lt}.
Goal forall (a : A), lt a a -> False.
Proof.
intros a H.
contradict (irreflexivity H).
Qed.
End defs.
|
