fix bit of proof broken by deletion of infer_e_complete_thm