The Coq mailing list

[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