Continued adding comments
More comments and minor fixes
Factored out code for Ind/Ind_eq checking
Moved Ind_eq of prop. equal to equal_path
Finished commenting Ind_eq, for now