knuton/la-girafe-sportive — pull request #2 by knuton (2013-12-09 19:51:19+00:00)
Title: 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.