Add some explorations in Subst module

I fixed some translation errors in the definition of `lift`, but the proof of the first lemma (`lift_lem1`) still does not go through.

For good reason, as the lemma is actually false. See example `fishy`, which actually translates into a proof of `lift_lem1`'s negation. We need to check whether this is a reasonable translation from the paper. Couldn't see a simple error in copying at least.