Following J.-L.~Krivine, we call $D$ the type inference system introduced by M.~Coppo and M.~Dezani where types are propositional formulae written with conjunction and implication from propositional letters --- there is no special constant $\omega$. We show here that the well-known result on $\cal D$, stating that any term which possesses a type in $\cal D$ strongly normalises does not need a new reducibility argument, but is a mere consequence of strong normalisation for natural deduction restricted to the conjunction and implication. The proof of strong normalisation for natural deduction, and therefore our result, as opposed to reducibility arguments, can be carried out within primitive recursive arithmetic. On the other hand, this enlighten the relation between $&$ and $\hat&$ that G.~Pottinger has already wondered about, and can be applied to other situations, like the lambda calculus with multiplicities of G.~Boudol.