My reading of that is that everything is made immutable, at which point aliasing isn't an issue anymore. I might be wrong though.

Author of that project here, it's the other way around - I'm using the absence oft aliasing to turn mutable Rust code immutable, which I can then embed in Lean. But you're right that ownership (ie, affine types) per se doesn't help.