@flancian @agora I think the OH is obviously true, and the FTOFFS has been proved, so there's no question there (the joke being that it's kind of hard to grok at first), and I think the FCH is true, but I'm less sure about it than about the first two