By the way, an argument for ex-falso which I found very compelling: Take "False" to be syntactic sugar for "0 = 1"; then you can prove by induction that if Fals

By the way, an argument for ex-falso which I found very compelling: Take "False" to be syntactic sugar for "0 = 1"; then you can prove by induction that if False then all numbers are equal. That gives you a great deal of quodlibet completely soundly (since by induction on list-length, all lists are then equal to the empty list, and so on).