Today I needed a formal proof of the FOL version of russell's paradox (not exists x forall y (E(x,y) iff not E(x,x))). When I tried to save the proof, my whole system crashed. See, these things matter! Jon