theory C imports A B
begin

end
