The Coq mailing list

[Amin Timany <amintimany AT gmail.com>]

In this case, you can simply use apply tactic as follows:

In

Г, H1 : Same_set A B, H2 : In A x |- _

"apply H1 in H2." results in:

Г, H1 : Same_set A B, H2 : In B x |- _

Amin

On 09 Jul 2014, at 15:11, Daniil Frumin 
<difrumin AT gmail.com>
 wrote:

> Hi, all
> 
> I was just curious about lack of facts for the Ensembles:
> http://coq.inria.fr/stdlib/Coq.Sets.Ensembles.html
> 
> Surely, there are a lot of small (but useful) theorems to state about sets.
> 
> Another thing I was actually wondering about, is the possibility of
> having rewrites using the Same_set as justifications.
> I mean going from
> 
> Г, Same_set A B, In A x |- _
> 
> to
> 
> Г, Same_set A B, In B x |- _
> 
> 
> I am not very familiar with Ltac to write it myself, but it does make
> sense to me.
> 
> Cheers
> 
> -- Daniil