The title is a bit misleading: you're not formally verifying rust's opaque types - you're simply proving a intuitionistic logic proposition using Coq. There's nothing Rust specific in that proof.
What would you have titled the blog instead to be less misleading?