Thank you for the lemmas, but your proofs are more complicated than is necessary and you may benefit from the following hints:
```
```
For a start, use ==> and not --> to separate assumptions from conclusions, your lemmas is easier to apply that way (and the proof is simpler because it avoids your rule+
```
Both proofs are found automatically by sledgehammer:

lemma map_addE1: "map_le f g ==> f++g = g"

lemma map_addE2: "map_le f g ==> (g++f = g)"

```
It is also possible to prove the statements by expanding the definitions (although that is usually not the best approach):
```
lemma map_addE1: "map_le f g ==> (f++g = g)"

The key trick here is to split the case expression automatically.

Tobias

On 08/09/2016 15:03, Andrea Giugliano wrote:
```
```Hello everyone,

I am working with the Map theory, and I found really useful these lemmas:

lemma map_addE1: "map_le f g --> (f++g = g)"
apply rule+
apply (case_tac " g x",force,force)
done

lemma map_addE2: "map_le f g --> (g++f = g)"
apply rule+
apply (case_tac " f x",force,force)
done

Maybe someone can add them to the Map theory?
Thanks,

Andrea Giugliano

```
```
```

Attachment: smime.p7s
Description: S/MIME Cryptographic Signature

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.