Relation between shallow and deep embedding of C.
For now we provide only a few theorems that relate notions from the shallow embedding with notions from the deep embedding. We plan to extend these at some point.