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