 The inference is sometimes called ex falso quodlibet or, more colorfully, explosion. Some call it “\(\neg\)-elimination”, but perhaps this stretches the notion of “elimination” a bit. We do not officially include ex falso quodlibet as a separate rule in \(D\), but as will be shown below (Theorem 10), each instance of it is derivable in our system \(D\).