Rewrite the theorem statement for infer_pes_complete and try to use it in Handle/Match cases
Proved most of infer_pes_complete