What is the Inversion Lemma
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.