-It would then turn out, for example, that `Vec::evil` is actually not a semantically well-typed function. It may leave an invalid `Vec` in `self`.
-This is just as bad as a function assigning `*b = 42` to a `b: &mut bool`.
-The only difference is that the compiler will catch the second example since it knows all about the semantics of `bool`. It doesn't know enough about the semantics of `Vec`.
+
+While proving soundness of `Vec`, it would then turn out that `Vec::evil` is actually not a semantically well-typed function. It may leave an invalid `Vec` in `self`.
+This is just as bad as a function assigning `*f = 42u32` to a `f: &mut f32`.
+The difference between `Vec` and `MyType` is no less significant than the difference between `f32` and `u32`.
+It's just that the compiler has been specifically taught about `f32`, while it doesn't know enough about the semantics of `Vec`.