diff --git a/cheatsheet.html b/cheatsheet.html
index ac21afd2a77f236222d3093672241e2bde0656bc..ceac4d557afd8007acaef73d34a370de2ad89104 100644
--- a/cheatsheet.html
+++ b/cheatsheet.html
@@ -46,16 +46,24 @@
 	</tr>
 	<tr>
 		<td>move: A</td>
-		<td>Move the assumption A from the context to the goal. If the goal was <code>G</code> before, it will be <code>A -> G</code> afterwards and <code>A</code> won't appear in the context anymore.</td>
+		<td>Move the assumption <code>A</code> from the context to the goal. If the goal was <code>G</code> before, it will be <code>A -> G</code> afterwards and <code>A</code> won't appear in the context anymore.</td>
 	</tr>
 	<tr>
 		<td>move /evP</td>
 		<td>Rephrase the top of the proof stack using the reflection lemma <code>evP</code>.</td>
 	</tr>
+	<tr>
+		<td>move /evP: H => H'</td>
+		<td>Rephrase the hypothesis <code>H</code> using the reflection lemma <code>evP</code> and store the result in the hypothesis <code>H'</code>.</td>
+	</tr>
 	<tr>
 		<td>move: {H}</td>
 		<td>Clear hypothesis <code>H</code>.</td>
 	</tr>
+	<tr>
+		<td>move Eq: expr => alias</td>
+		<td>Replace <code>expr</code> with the name <code>alias</code> and store the according equation in the new hypothesis <code>Eq</code>.</td>
+	</tr>
 	<tr>
 		<td>case: m</td>
 		<td>Destruct <code>m</code>, which must be inductively defined (This includes propositions). Creates one subgoal for every constructor. Note: <code>m</code> may be a complex expression, as long as its type is inductive. TODO: <code>case</code> also calls <code>injection</code>.</td>
@@ -84,6 +92,10 @@
 		<td>case E': n.+2 / E</td>
 		<td>Like <code>case E': n.+2 /</code>, but performs the case analysis in hypothesis <code>E</code></tr>
 	</tr>
+	<tr>
+		<td>case H: _ _ _ /</td>
+		<td>TODO</td>
+	</tr>
 	<tr>
 		<td>case n //</td>
 		<td>Do a case analysis on <code>n</code> and resolve the trivial subgoals.</td>
@@ -220,6 +232,34 @@
 		<td>omega</td>
 		<td>Solve most arithmetic expressions with <code>+</code>, <code>-</code>, and <code>*</code>.</td>
 	</tr>
+	<tr>
+		<td>invas</td>
+		<td>Invert and substitute.</td>
+	</tr>
+	<tr>
+		<td>eauto</td>
+		<td>Try to solve the goal by applying lemmas, unfolding definitions.</td>
+	</tr>
+	<tr>
+		<td>eauto with ImpDB</td>
+		<td>Try to solve the goal by applying lemmas, unfolding definitions. Take hints from <code>ImpDB</code>.</td>
+	</tr>
+	<tr>
+		<td>eauto using lemma1, lemma2</td>
+		<td>Try to solve the goal by applying lemmas, unfolding definitions. Add <code>lemma1</code>, <code>lemma2</code> to the lists of lemmas to apply.</td>
+	</tr>
+	<tr>
+		<td>tauto</td>
+		<td>TODO</td>
+	</tr>
+	<tr>
+		<td>solve</td>
+		<td>TODO</td>
+	</tr>
+	<tr>
+		<td>eexists</td>
+		<td>Apply constructor of exists with holes.</td>
+	</tr>
 </table>
 
 <h1>Tacticals</h1>