The Coq mailing list

[Holden Lee <hl422 AT cam.ac.uk>]

Beginner's question: I have a lemma that intersection with the empty set is empty:

Lemma int_empty :

forall (Y: Ensemble U), 

    (Intersection U (Empty_set U) Y) = Empty_set U.

During a later proof I have as a goal

cardinal U Y n ->

cardinal U (Intersection U (Empty_set U) Y) p ->

cardinal U (Union U (Empty_set U) Y) (0 + n - p)

I would like to replace Intersection U (Empty_set U) Y with Empty_set U. How do I do this? rewrite int_empty gives: Error: The reference int_empty was not found in the current environment.

-Holden