Several changes

- Experimenting with new formulation of Subst, EProver, etc.
- Remove requirement for Safe_expr and just define it based on exprD'
  - This avoids the need to have it everywhere
  - Merging some proofs
- Moved FMapSubst but it isn't migrated yet.
- Some progress on AutoProver2/3 but they still aren't done.
  It may be necessary to do the proofs in two parts, or maybe
  I just need to give a better specification to all_success.
- TODO: There's a new (stratified) lemmaD which I think will be
  cleaner and more useful.
autoprover3 is sound (modulo weakening)

- proof was more complex than i thought it would be