Add Parametric Morphism: elem_morph

[awalterschulze]

We added another parametric morphism to our setoid, which allows us to reuse rewrite rules that are in lang_iff and apply them to iff with \in, which was frustratingly not possible before:

Add Parametric Morphism {s}: (elem s)
  with signature lang_iff ==> iff
  as elem_morph.

For example:

  forall (p q: regex)
  (pq: {{p}} {<->} {{q}}),
  forall s: str,
  s \in {{q}} <-> s \in {{p}}.

This should help to simplify the commutes_concat_a proof going forward.