(*#* This is a proof in the pure Calculus of Construction that
classical logic in Prop + dependent elimination of disjunction entails
(*#* This is a proof in the pure Calculus of Construction that
classical logic in Prop + dependent elimination of disjunction entails