-
@TienChihMath I think exhaustion is when you show P holds for any of the statements Sn for which OR(Sn) is true. I'm suggesting that we are proving a statement Si (the Mousekatool is the best tool) by showing each Sj is false (leads to a contradiction).