The Coq mailing list

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

That was it actually. Thanks.

-Holden

2014-08-27 17:25 GMT+01:00 Jonathan <jonikelee AT gmail.com>:

On 08/27/2014 03:57 AM, Holden Lee wrote:

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

It would help if we could see what happened in between.  For instance, did you completely finish the proof of int_empty (with Qed)?

-- Jonathan