some renaming of theorems
added inverse of inverse path is the path itself