It gives you the proof that's loosely stated as "well-types programs do not go wrong". The sketch is that if some thing is well-typed then progress means it won

It gives you the proof that's loosely stated as "well-types programs do not go wrong". The sketch is that if some thing is well-typed then progress means it won't "go wrong" and preservation means it'll stay well-typed. Thus: well-typed programs progress all the way to stable values.