Proof of Cntl theorem (w/ cheating). Several bugfixes in the model
that occured during this proof.
Formulated an important lemma.