updating CK instantiation
fixing intermediate theories, adding parameters and rewriting some of the interpretations - proof of two TCCs
completed proof of add optional feature