theory E imports C D begin end