theory E imports C D
begin

end
