A many-sorted natural deduction