Write down (and prove) and inversion lemma

[aigarashi]

This is a nitty gritty technical detail, but we must cross our t's and dot our i's.