Interpolation and definability in some modal Heyting Brouwer logics