blob: 01e35810b0eb3090544c6a09c48cf6b6adf37c55 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
|
Require Import Setoid Coq.Classes.Morphisms.
Set Typeclasses Legacy Resolution.
Declare Instance and_Proper_eq: Proper (Logic.eq ==> Logic.eq ==> Logic.eq) and.
Axiom In : Prop.
Axiom union_spec : In <-> True.
Lemma foo : In /\ True.
Proof.
progress rewrite union_spec.
repeat constructor.
Qed.
|
