Used the terminating version of subst in compute_semanticsLib and remove a superfluous case in proof