theory C imports A B begin end