§ Coq Cheat Sheet
Things in Coq that I keep forgetting, and are hard to lookup.
§ Manually set the value of an existential
instantiate
§ Rename an expression with an identifier throughout the proof
set (ident := expr) in *
This is useful to not lose information when destruct ing.