For anyone else for whom the justification for “either x and f(f(x)) are both red, or f(x) and f(f(f(x)) are both red” was not immediately obvious: H: ∀x.(r(x)

For anyone else for whom the justification for “either x and f(f(x)) are both red, or f(x) and f(f(f(x)) are both red” was not immediately obvious: H: ∀x.(r(x)→⊥)→r(f(x)) goal: ∃x.r(x)∧r(f(f(x))) If f(f(x)) is red: x is a solution (QED). Otherwise: f(f(x)) not being red means f(x) must have been (by contraposition of H) and that f(f(f(x))) will be (by H); therefore, f(x) is a solution.