proved renaming product theorem
finished proving renaming laws