I don't want to make it seem like I'm proving anything novel here, the proof I work through is definitely pretty basic as far as proofs go. It's written somewhat narratively because it reflects a train of thought I went through a few days ago when reading about existential types in Rust. Seeing the theorem ((∃ x. P(x)) → Q) ⇔ (∀ x. (P(x) → Q)) in the blog post made me want see if I still remembered enough Coq to prove it, and then when I was sitting down this morning to write something I thought it would make a good blog post as it explores some deep cuts of what I've been learning in Rust and might make a good introduction for people into Coq. I'll definitely take it on the chin that I titled the blog too ambitiously however and I'll be more modest with my titles in the future.