update proof of pat_to_pat_correct