check

doc/CheatSheet.md

@@ -1,6 +1,11 @@
 
 
-| 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` | 
+| Formula        |  Prove        | Use      |
+| -------------- | ------------- | -------- |
+| `true`         | `.`           | No uses  |
+| `false`        | [Contradiction](./Reference.md#contradiction) | implicit as anything |
+| `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` | 
+| `if P then Q` | [`assume`](./Reference.md#assume) | [`apply`-`to`](./Reference.md#apply-to-proof-modus-ponens) |
+
+

doc/Reference.md

@@ -435,6 +435,35 @@ proof
 end
 ```
 
+## Contradiction
+
+During a proof, one sometimes encounters assumptions that contradict
+each other. In these situations, you can prove `false` and from that,
+anything else (the Principle of Explosion). Here are two ways to prove
+`false` from contradictions.
+
+(1) If you have a proof `X` of an equality with different constructors
+on the left and right-hand side, such as
+
+```
+have X: empty = Node(3, empty) by ...
+```
+
+then you can implicitly use `X` to prove `false`:
+
+```
+conclude false by X
+```
+
+(2) If you have a proof `X` of `P` and a proof `Y` of `not P`,
+then you can prove `false` using `apply`-`to`. (Because
+`not P` is shorthand for `if P then false`.)
+
+```
+have X: P by ...
+have Y: not P by ...
+conclude false by apply Y to X
+``
 
 ## Define (Statement)