Add lemmas in modalities.v ; solve nj_inter_equiv