Prove the important completeness result about the case-ambiguity.
Use the previous commit's completeness result; also do another easy case.

37 (mostly easy?) cases to go.