Fixed #118 (two theorems called [equiv_path_inverse]).