Still not necessarily true.
The academic usage holds that the distinction between the true type systems and the pretenders is that the first are sound: a well-typed program either evaluates to a normal form (value) or fails to terminate, but can never get stuck (segfault, terminate with an uncaught exception, however your environment implements that).
Of course, a gradual system like Mypy can never both be sound in this sense and remain gradual (which is a major selling point for Mypy), so for them the rule is usually amended with “provided the program is fully annotated” (and it should be obvious whether any given program is fully annotated or not, otherwise the system is just user-hostile regardless of how sound it is; at the very least it must be decidable). That is still obviously not satisfied for Mypy, because it doesn’t track exceptions (and including uncaught exceptions in normal forms would be useless because then no Python programs would ever get stuck). The actual guarantee Mypy is supposed to provide sounds kind of wimpy, like “never gets a TypeError that is not explicitly raised in user code”, but would still be useful regardless... Except that soundness is usually a pretty non-trivial theorem, and the lack of a readable specification for Mypy’s type system precludes it from being proven.
While well-typed Haskell (or SML) programs can in fact crash from the user’s perspective, the possible sources of crashes are rare and avoidable enough (for Haskell, only non-exhaustive patterns and explicit use of undefined, error, or throw) that you can call them additional normal forms without making the whole thing trivial. Every other way an untyped program could get stuck is disallowed by the type system, and there is a proof (SML) or at least a proof sketch (Haskell) of that (although of course not every untyped program that can’t get stuck is allowed by the type system, that is impossible by Turing—Gödel). Even the horrendously complicated systems that GHC implements nowadays still have papers that prove their soundness for a good enough toy example that one walks away convinced that the real thing works just as well.
So yes, there is a sense in which Mypy’s system is less “true” than SML’s or Haskell’s, and it is directly caused by (though not completely reducible to) the lack of a complete human-readable spec for both Mypy and Python itself. (I love Python to bits, but its object model is surreal and its only complete description is Objects/object.c together with Objects/typeobject.c.) If a wizard waved his wand and made every copy of the Haskell Report disappear, its type system would technically remain sound, but illegibly so to human mathematicians, thus it would in fact become less “true” in this sense than previously. Multiple implementations help, but I expect that without a prose spec it wouldn’t be easy to tell that GHC, UHC and Hugs implement the same system, the same way I have no idea if Mypy and Pytype do.