diff --git a/doc/CheatSheet.md b/doc/CheatSheet.md
new file mode 100644
index 0000000..e440ca3
--- /dev/null
+++ b/doc/CheatSheet.md
@@ -0,0 +1,6 @@
+
+
+| Formula    |  Prove        | Use      |
+| ---------- | ------------- | -------- |
+| `P and Q`  |  `,` [Comma](./Reference.md#comma-conjunction-and-introduction)) | (1) implicit as `P` (2) implicit as `Q` |
+| `P or Q`   | (1) implicit from `P` (2) implicit from `Q` | 
diff --git a/ex/Sum.pf b/ex/Sum.pf
index 5f6ad72..e6c1772 100644
--- a/ex/Sum.pf
+++ b/ex/Sum.pf
@@ -90,4 +90,4 @@ proof
         = summation(length(xs), 0, nth(xs,0)) + summation(length(ys), 0, nth(ys,0))
       by apply summation_add[length(xs)][length(ys), 0, 0, nth(xs ++ ys, 0), nth(xs,0), nth(ys,0)]
          to p1, p2
-end
\ No newline at end of file
+end