Automate the strong injection theorem

Required for e.g. renaming in codatatypes, useful in general. Example proof is available [here](https://github.com/jvanbruegge/binder_datatypes/blob/1a1d8518ea8e79b260957a3f0c7bbd4e7388a9cd/operations/VVSubst_Corec.thy#L8). Should be part of the fixpoint construction in `mrbnf_fp.ML`