Bug fix: setup_proof gave error on no input, and didn't switch from prbt to appt for proofs with no premises (theorems)