diff --git a/.github/example.png b/.github/example.png
new file mode 100644
index 0000000..e893d74
Binary files /dev/null and b/.github/example.png differ
diff --git a/README.md b/README.md
index ea902b6..c0dc141 100644
--- a/README.md
+++ b/README.md
@@ -1,5 +1,5 @@
 <p align="center">
-<!-- <img src=".github/logo.png" width="512"> -->
+<img src=".github/example.png", width = 512>
 </p>
 <h3 align="center">A Fitch-style natural deduction proof checker, with support for modal logic.</h3>
 
@@ -14,20 +14,22 @@
   - TFL (basic and derived rulesets)
   - Modal logic (systems $K$, $T$, $S_4$, and $S_5$)
 - Cross-platform thanks to `egui`; runs on all major operating systems and in the browser
+- Keyboard shortcuts and automatic checker execution
 
 ## Installation
 
+### Web Version
+Deduct is available as a web app [here](https://colonial-dev.github.io/deduct/). Use a laptop or desktop for the best experience.
+
 ### Precompiled Binaries
 Precompiled versions of Deduct are available for:
 - Windows
 - macOS
 - Linux (compiled against `x86_64-unknown-linux-musl`, which should Just Work™ on most distributions.) 
-- WebAssembly (runs in your browser.)
 
 All binaries can be found in the [releases](https://github.com/Colonial-Dev/deduct/releases) section.
 
 ### From Source
-
 Dependencies:
 - The [Rust programming language](https://rustup.rs/).
 - A C/C++ toolchain (such as `gcc`.)
@@ -38,8 +40,18 @@ cargo install --locked --git https://github.com/Colonial-Dev/deduct --branch mas
 ```
 
 ## Getting Started
-
-## Design
+You can start a new proof by navigating to `Proof` > `New...` in the menu bar. Select which rulesets you'd like to enable, enter your premises (if any) and conclusion, and hit `Create proof`. If your sentences are well formed, the window will close and you can start working on the proof.
+
+### Tips
+- If you would prefer light mode or a larger UI, both can be adjusted under `Preferences` in the menu bar. Your choices will be remembered even if you close and re-open Deduct.
+- You can review logical operator shorthands and proof rules in the sidebar.
+- You can restart the proof and change your argument (if needed) under the `Proof` dropdown in the menu bar.
+
+### Control
+- You can add and remove lines or subproofs by hovering over the relevant line and clicking the buttons that appear to the right of the citation field.
+- All insertion actions also have keyboard shortcuts. The exact keys vary between platforms; look at `Help` > `Shortcuts` in the menu bar to find yours.
+- Whenever you edit a field or remove a line, the proof checker will automatically execute and display its output at the bottom of the window. 
+  - (Adding a line or subproof does not trigger the checker.)
 
 ## Acknowledgements
 Thank you to: