diff --git a/cheatsheet.html b/cheatsheet.html
index 27a06582d4b7e1d3c79fc3d878c7eb9ecb333913..2e3520abd62493c1b2cdd4a1ad4cb56688fa242a 100644
--- a/cheatsheet.html
+++ b/cheatsheet.html
@@ -50,7 +50,7 @@
 	</tr>
 	<tr>
 		<td>move /evP</td>
-		<td>...</td>
+		<td>Rephrase the top of the proof stack using the reflection lemma <code>evP</code>.</td>
 	</tr>
 	<tr>
 		<td>case: m</td>
@@ -73,16 +73,20 @@
 		<td>Destruct <code>m</code> and remember information about the current branch in the hypothesis <code>H</code>.</td>
 	</tr>
 	<tr>
-		<td>case n.+2 / E</td>
-		<td>...</td>
+		<td>case E': n.+2 /</td>
+		<td>Assume the goal is <code>ev x.+2 -> ev x</code>. Do a case analysis on the arguments of the inductive type <code>ev</code> (Which is defined as <code>Inductive ev: nat -> Prop := ev_0: ev 0 | ev_SS: ev n -> ev n.+2</code>) and remember information about the case analysis in <code>E'</code>. This produces two new goals, one for the constructor <code>ev_0</code> with <code>E: x.+2 = 0</code> and one for the constructor <code>ev_SS</code> with <code>E: x.+2 = n.+2<code> and evidence for <code>ev n</code>.</td>
+	</tr>
+	<tr>
+		<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 n //</td>
 		<td>Do a case analysis on <code>n</code> and resolve the trivial subgoals.</td>
 	</tr>
 	<tr>
-		<td>case: H1 Hn => <-</td>
-		<td>...</td>
+		<td>case: H => <-</td>
+		<td>Do a case analysis on the equation <code>H</code>, move the result to the context, rewrite with it, and forget about it.</td>
 	</tr>
 	<tr>
 		<td>case</td>
@@ -98,7 +102,7 @@
 	</tr>
 	<tr>
 		<td>apply/evenP</td>
-		<td>...</td>
+		<td>Rephrase the goal using the reflection lemma <code>evenP</code>.</td>
 	</tr>
 	<tr>
 		<td>apply</td>