That is, duplicate lemmas making use of an algebraic type (either by using a projection, a constructor or a pattern matching) which is tagged by the new meta alginst.

Also:
- Add new select metas for automatically tagging types with alginst
- edit relevent drivers so that discrimination happens before eliminate_algebraic:
    - CVC5
    - Z3 > 4.8.7
    - Vampire 4.5.1
    - why3-smt