update proof of row_to_pat_correct