Links: [[Coq]] Good overview of important tactics and proof approaches https://pjreddie.com/coq-tactics/#unfold Tactic cheat sheet https://www.cs.cornell.edu/courses/cs3110/2018sp/a5/coq-tactics-cheatsheet.html Coq cheat cheet http://www.inf.ed.ac.uk/teaching/courses/tspl/cheatsheet.pdf - `rewrite` use a theorem about a relation (usually an equality) to rewrite one hand side to the other. - `apply` ?