I am taking a programming languages course, and we have had to use the Inversion Lemma many times in our proofs of preservation. We have been given the Inversion Lemma in each of these examples, but is there a general statement of the inversion lemma that can be applied to any proof of preservation? Can someone write that out for me/explain it a little bit?
When you have a collection of rules, an inversion lemma lets you prove the premises of a rule from the conclusion. You can't just assume that inversion is true. You have to prove it by rule induction. However, classes will often give it to you because it is often tedious and easy to prove. The reason inversion doesn't always work is that there may be multiple rules which match the conclusion you are trying to use inversion on, and then you only know that the premises of one of those rules is true, but not which rule.