I think the terms normally used for this is "completeness" and "soundness", as in, the D type system is "sound" because it rejects all programs with use-after-free, but it is "incomplete" because there are some programs that cannot exhibit use-after-free for any input values, but that the type system rejects.

Given these more precise definitions, the analogous theorem would be that there is no type system (or static analysis) for use-after-free which is both sound and complete.