Intuitively, this means one would not like to write a expression, in say Haskell, of type Int, and have it evaluate to a value v, only to find out that v is a string.
Together with progress, it is an important meta-theoretical property for establishing type soundness of a type system.
The opposite property, if Γ ⊢ e2 : τ and e1 → e2 then Γ ⊢ e1 : τ, is called subject expansion.
It often does not hold as evaluation can erase ill-typed sub-terms of an expression, resulting in a well-typed one.
This programming language theory or type theory-related article is a stub.