attempt to make some progress on repl_fun_alt_proof

But I don't understand the point of the main theorems, or how they were
originally made, so haven't figured out how to update them.