§ 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.