Fixed infer_pes thm statement and proved the cheat, prove Handle as well