[a-nikolaev]

You misunderstand my comment. I'm not saying that your interpretation is wrong. I'm fine with it. Better or not, either result can be used in the right context. I'm saying that your interpretation does not eliminate disjunction, so it should be called differently. It's a different rule, that's all I want to say.

[thaumasiotes]

> Better or not, either result can be used in the right context.

This is most of the point I'm making -- there is no context where the brittle, overspecified version is useful but the more general version isn't. But there are lots of contexts where the overspecified version is useless.

And again, it's not a different rule. Brittle "disjunction elimination" is a special case of the rule I state. Similarly, the Pythagorean Theorem is a special case of the Law of Cosines, not a different rule.

It gets worse, though, because where the Pythagorean Theorem is simpler to state than the Law of Cosines, brittle disjunction elimination is more complex to state than the more general result is.

Think about exportation. We say:

    (a implies (b implies p)) iff ((a and b) implies p)

We don't say:

    ((a implies (b implies p)) and (a and b)) implies p

That second version, which is the equivalent of brittle disjunction elimination for and instead of or, is harder to state, is less informative, and doesn't generalize.