A small bit of conLang progress

Factor out two lemmas (currently cheated) about disjointness of the
constructor exhaustivity maps. There is now only 1 cheat in the main
theorem.