The Coq mailing list

[Ryan Wisnesky <ryan AT cs.harvard.edu>]

One trick I've found is that if you have functional and propositional 
extensionality available, it's easy to replace the inductive definitions from 
Ensembles with equivalent but more computational versions, for example:

Lemma union_def : forall a (f g : Ensemble a),
 Union f g = fun x : a => f x \/ g x.

For my purposes, I found the computational versions to be much easier to work 
with.

On Nov 3, 2013, at 7:00 AM, Volker Stolz 
<stolz+coq AT ifi.uio.no>
 wrote:

> Good evening everyone,
> I just found myself defining and proving a handful of lemmas over
> Ensemble-operations, and I doubt I already have all that I'll need.
> 
> Maybe someone already has a nice collection of them that she'd like to
> share (going beyond those in Powerset_facts)?
> 
>  -Volker