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.
Merge remote-tracking branch 'origin/master' into tup+eq