diff --git a/Cargo.lock b/Cargo.lock
index 035cd98..b00d8bd 100644
--- a/Cargo.lock
+++ b/Cargo.lock
@@ -835,12 +835,19 @@ version = "1.1.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "96a6ac251f4a2aca6b3f91340350eab87ae57c3f127ffeb585e92bd336717991"
 
+[[package]]
+name = "data-url"
+version = "0.3.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "5c297a1c74b71ae29df00c3e22dd9534821d60eb9af5a0192823fa2acea70c2a"
+
 [[package]]
 name = "deduct"
 version = "1.0.0"
 dependencies = [
  "eframe",
  "egui",
+ "egui_extras",
  "once_cell",
  "regex",
  "serde",
@@ -1020,6 +1027,22 @@ dependencies = [
  "winit",
 ]
 
+[[package]]
+name = "egui_extras"
+version = "0.27.2"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "1b78779f35ded1a853786c9ce0b43fe1053e10a21ea3b23ebea411805ce41593"
+dependencies = [
+ "egui",
+ "ehttp",
+ "enum-map",
+ "image",
+ "log",
+ "mime_guess2",
+ "resvg",
+ "serde",
+]
+
 [[package]]
 name = "egui_glow"
 version = "0.27.2"
@@ -1036,6 +1059,20 @@ dependencies = [
  "winit",
 ]
 
+[[package]]
+name = "ehttp"
+version = "0.5.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "59a81c221a1e4dad06cb9c9deb19aea1193a5eea084e8cd42d869068132bf876"
+dependencies = [
+ "document-features",
+ "js-sys",
+ "ureq",
+ "wasm-bindgen",
+ "wasm-bindgen-futures",
+ "web-sys",
+]
+
 [[package]]
 name = "emath"
 version = "0.27.2"
@@ -1046,6 +1083,27 @@ dependencies = [
  "serde",
 ]
 
+[[package]]
+name = "enum-map"
+version = "2.7.3"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "6866f3bfdf8207509a033af1a75a7b08abda06bbaaeae6669323fd5a097df2e9"
+dependencies = [
+ "enum-map-derive",
+ "serde",
+]
+
+[[package]]
+name = "enum-map-derive"
+version = "0.17.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "f282cfdfe92516eb26c2af8589c274c7c17681f5ecc03c18255fe741c6aa64eb"
+dependencies = [
+ "proc-macro2",
+ "quote",
+ "syn 2.0.57",
+]
+
 [[package]]
 name = "enumflags2"
 version = "0.7.9"
@@ -1210,6 +1268,12 @@ dependencies = [
  "miniz_oxide",
 ]
 
+[[package]]
+name = "float-cmp"
+version = "0.9.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "98de4bbd547a563b716d8dfa9aad1cb19bfab00f4fa09a6a4ed21dbcf44ce9c4"
+
 [[package]]
 name = "foreign-types"
 version = "0.5.0"
@@ -1571,6 +1635,12 @@ dependencies = [
  "png",
 ]
 
+[[package]]
+name = "imagesize"
+version = "0.12.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "029d73f573d8e8d63e6d5020011d3255b28c3ba85d6cf870a07184ed23de9284"
+
 [[package]]
 name = "indexmap"
 version = "2.2.6"
@@ -1658,6 +1728,15 @@ version = "3.1.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "e2db585e1d738fc771bf08a151420d3ed193d9d895a36df7f6f8a9456b911ddc"
 
+[[package]]
+name = "kurbo"
+version = "0.9.5"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "bd85a5776cd9500c2e2059c8c76c3b01528566b7fcbaf8098b55a33fc298849b"
+dependencies = [
+ "arrayvec",
+]
+
 [[package]]
 name = "libc"
 version = "0.2.153"
@@ -1796,6 +1875,22 @@ dependencies = [
  "paste",
 ]
 
+[[package]]
+name = "mime"
+version = "0.3.17"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "6877bb514081ee2a7ff5ef9de3281f14a4dd4bceac4c09388074a6b5df8a139a"
+
+[[package]]
+name = "mime_guess2"
+version = "2.0.5"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "25a3333bb1609500601edc766a39b4c1772874a4ce26022f4d866854dc020c41"
+dependencies = [
+ "mime",
+ "unicase",
+]
+
 [[package]]
 name = "miniz_oxide"
 version = "0.7.2"
@@ -2067,6 +2162,12 @@ version = "2.3.1"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "e3148f5046208a5d56bcfc03053e3ca6334e51da8dfb19b6cdc8b306fae3283e"
 
+[[package]]
+name = "pico-args"
+version = "0.5.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "5be167a7af36ee22fe3115051bc51f6e6c7054c9348e28deb4f49bd6f705a315"
+
 [[package]]
 name = "pin-project-lite"
 version = "0.2.14"
@@ -2252,6 +2353,12 @@ version = "0.6.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "42a9830a0e1b9fb145ebb365b8bc4ccd75f290f98c0247deafbbe2c75cefb544"
 
+[[package]]
+name = "rctree"
+version = "0.5.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "3b42e27ef78c35d3998403c1d26f3efd9e135d3e5121b0a4845cc5cc27547f4f"
+
 [[package]]
 name = "redox_syscall"
 version = "0.3.5"
@@ -2316,6 +2423,44 @@ version = "1.1.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "19b30a45b0cd0bcca8037f3d0dc3421eaf95327a17cad11964fb8179b4fc4832"
 
+[[package]]
+name = "resvg"
+version = "0.37.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "cadccb3d99a9efb8e5e00c16fbb732cbe400db2ec7fc004697ee7d97d86cf1f4"
+dependencies = [
+ "log",
+ "pico-args",
+ "rgb",
+ "svgtypes",
+ "tiny-skia",
+ "usvg",
+]
+
+[[package]]
+name = "rgb"
+version = "0.8.37"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "05aaa8004b64fd573fc9d002f4e632d51ad4f026c2b5ba95fcb6c2f32c2c47d8"
+dependencies = [
+ "bytemuck",
+]
+
+[[package]]
+name = "ring"
+version = "0.17.8"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "c17fa4cb658e3583423e915b9f3acc01cceaee1860e33d59ebae66adc3a2dc0d"
+dependencies = [
+ "cc",
+ "cfg-if",
+ "getrandom",
+ "libc",
+ "spin",
+ "untrusted",
+ "windows-sys 0.52.0",
+]
+
 [[package]]
 name = "ron"
 version = "0.8.1"
@@ -2328,6 +2473,12 @@ dependencies = [
  "serde_derive",
 ]
 
+[[package]]
+name = "roxmltree"
+version = "0.19.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "3cd14fd5e3b777a7422cca79358c57a8f6e3a703d9ac187448d0daf220c2407f"
+
 [[package]]
 name = "rustc-hash"
 version = "1.1.0"
@@ -2361,6 +2512,37 @@ dependencies = [
  "windows-sys 0.52.0",
 ]
 
+[[package]]
+name = "rustls"
+version = "0.22.4"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "bf4ef73721ac7bcd79b2b315da7779d8fc09718c6b3d2d1b2d94850eb8c18432"
+dependencies = [
+ "log",
+ "ring",
+ "rustls-pki-types",
+ "rustls-webpki",
+ "subtle",
+ "zeroize",
+]
+
+[[package]]
+name = "rustls-pki-types"
+version = "1.5.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "beb461507cee2c2ff151784c52762cf4d9ff6a61f3e80968600ed24fa837fa54"
+
+[[package]]
+name = "rustls-webpki"
+version = "0.102.3"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "f3bce581c0dd41bce533ce695a1437fa16a7ab5ac3ccfa99fe1a620a7885eabf"
+dependencies = [
+ "ring",
+ "rustls-pki-types",
+ "untrusted",
+]
+
 [[package]]
 name = "same-file"
 version = "1.0.6"
@@ -2452,6 +2634,21 @@ version = "0.3.7"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "d66dc143e6b11c1eddc06d5c423cfc97062865baf299914ab64caa38182078fe"
 
+[[package]]
+name = "simplecss"
+version = "0.2.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "a11be7c62927d9427e9f40f3444d5499d868648e2edbc4e2116de69e7ec0e89d"
+dependencies = [
+ "log",
+]
+
+[[package]]
+name = "siphasher"
+version = "0.3.11"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "38b58827f4464d87d377d175e90bf58eb00fd8716ff0a62f80356b5e61555d0d"
+
 [[package]]
 name = "slab"
 version = "0.4.9"
@@ -2531,6 +2728,12 @@ dependencies = [
  "winapi",
 ]
 
+[[package]]
+name = "spin"
+version = "0.9.8"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "6980e8d7511241f8acf4aebddbb1ff938df5eebe98691418c4468d0b72a96a67"
+
 [[package]]
 name = "spirv"
 version = "0.3.0+sdk-1.3.268.0"
@@ -2551,6 +2754,25 @@ name = "strict-num"
 version = "0.1.1"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "6637bab7722d379c8b41ba849228d680cc12d0a45ba1fa2b48f2a30577a06731"
+dependencies = [
+ "float-cmp",
+]
+
+[[package]]
+name = "subtle"
+version = "2.5.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "81cdd64d312baedb58e21336b31bc043b77e01cc99033ce76ef539f78e965ebc"
+
+[[package]]
+name = "svgtypes"
+version = "0.13.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "6e44e288cd960318917cbd540340968b90becc8bc81f171345d706e7a89d9d70"
+dependencies = [
+ "kurbo",
+ "siphasher",
+]
 
 [[package]]
 name = "syn"
@@ -2626,6 +2848,7 @@ dependencies = [
  "bytemuck",
  "cfg-if",
  "log",
+ "png",
  "tiny-skia-path",
 ]
 
@@ -2746,6 +2969,15 @@ dependencies = [
  "winapi",
 ]
 
+[[package]]
+name = "unicase"
+version = "2.7.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "f7d2d4dafb69621809a81864c9c1b864479e1235c0dd4e199924b9742439ed89"
+dependencies = [
+ "version_check",
+]
+
 [[package]]
 name = "unicode-bidi"
 version = "0.3.15"
@@ -2785,6 +3017,29 @@ version = "0.2.4"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "f962df74c8c05a667b5ee8bcf162993134c104e96440b663c8daa176dc772d8c"
 
+[[package]]
+name = "untrusted"
+version = "0.9.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "8ecb6da28b8a351d773b68d5825ac39017e680750f980f3a1a85cd8dd28a47c1"
+
+[[package]]
+name = "ureq"
+version = "2.9.6"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "11f214ce18d8b2cbe84ed3aa6486ed3f5b285cf8d8fbdbce9f3f767a724adc35"
+dependencies = [
+ "base64",
+ "flate2",
+ "log",
+ "once_cell",
+ "rustls",
+ "rustls-pki-types",
+ "rustls-webpki",
+ "url",
+ "webpki-roots",
+]
+
 [[package]]
 name = "url"
 version = "2.5.0"
@@ -2796,6 +3051,50 @@ dependencies = [
  "percent-encoding",
 ]
 
+[[package]]
+name = "usvg"
+version = "0.37.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "38b0a51b72ab80ca511d126b77feeeb4fb1e972764653e61feac30adc161a756"
+dependencies = [
+ "base64",
+ "log",
+ "pico-args",
+ "usvg-parser",
+ "usvg-tree",
+ "xmlwriter",
+]
+
+[[package]]
+name = "usvg-parser"
+version = "0.37.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "9bd4e3c291f45d152929a31f0f6c819245e2921bfd01e7bd91201a9af39a2bdc"
+dependencies = [
+ "data-url",
+ "flate2",
+ "imagesize",
+ "kurbo",
+ "log",
+ "roxmltree",
+ "simplecss",
+ "siphasher",
+ "svgtypes",
+ "usvg-tree",
+]
+
+[[package]]
+name = "usvg-tree"
+version = "0.37.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "8ee3d202ebdb97a6215604b8f5b4d6ef9024efd623cf2e373a6416ba976ec7d3"
+dependencies = [
+ "rctree",
+ "strict-num",
+ "svgtypes",
+ "tiny-skia-path",
+]
+
 [[package]]
 name = "version_check"
 version = "0.9.4"
@@ -3036,6 +3335,15 @@ dependencies = [
  "web-sys",
 ]
 
+[[package]]
+name = "webpki-roots"
+version = "0.26.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "b3de34ae270483955a94f4b21bdaaeb83d508bb84a01435f393818edb0012009"
+dependencies = [
+ "rustls-pki-types",
+]
+
 [[package]]
 name = "wgpu"
 version = "0.19.4"
@@ -3558,6 +3866,12 @@ version = "0.8.20"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "791978798f0597cfc70478424c2b4fdc2b7a8024aaff78497ef00f24ef674193"
 
+[[package]]
+name = "xmlwriter"
+version = "0.1.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "ec7a2a501ed189703dba8b08142f057e887dfc4b2cc4db2d343ac6376ba3e0b9"
+
 [[package]]
 name = "zbus"
 version = "3.15.2"
@@ -3644,6 +3958,12 @@ dependencies = [
  "syn 2.0.57",
 ]
 
+[[package]]
+name = "zeroize"
+version = "1.7.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "525b4ec142c6b68a2d10f01f7bbf6755599ca3f81ea53b8431b7dd348f5fdb2d"
+
 [[package]]
 name = "zvariant"
 version = "3.15.2"
diff --git a/Cargo.toml b/Cargo.toml
index 0005217..d5a83b4 100644
--- a/Cargo.toml
+++ b/Cargo.toml
@@ -31,6 +31,7 @@ thiserror = "1.0.58"
 once_cell = "1.19.0"
 regex = "1.10.3"
 serde = { version = "1.0.197", features = ["derive"] }
+egui_extras = { version = "0.27.2", features = ["all_loaders"] }
 
 # Addl. WASM dependencies
 [target.'cfg(target_arch = "wasm32")'.dependencies]
diff --git a/src/main.rs b/src/main.rs
index 7c505c9..a568d32 100644
--- a/src/main.rs
+++ b/src/main.rs
@@ -6,8 +6,8 @@ mod ui;
 fn main() {
     let native_options = eframe::NativeOptions {
         viewport: egui::ViewportBuilder::default()
-            .with_inner_size([720.0, 720.0])
-            .with_min_inner_size([720.0, 720.0]),
+            .with_inner_size([1024.0, 720.0])
+            .with_min_inner_size([1024.0, 720.0]),
             // TODO add icon
         ..Default::default()
     };
diff --git a/src/ui/mod.rs b/src/ui/mod.rs
index 29c9de7..4126422 100644
--- a/src/ui/mod.rs
+++ b/src/ui/mod.rs
@@ -46,6 +46,8 @@ pub struct Deduct {
 
 impl Deduct {
     pub fn new(cc: &eframe::CreationContext<'_>) -> Self {
+        egui_extras::install_image_loaders(&cc.egui_ctx);
+
         fonts_init(cc);
 
         if let Some(storage) = cc.storage {
@@ -68,8 +70,8 @@ impl Deduct {
         if let Some(ui) = self.new.try_create() {
             self.proof = Some(ui);
             self.vis.new_proof = false;
-            self.new.ready = false;
         }
+        self.new.ready = false;
     }
 
     fn handle_shortcuts(&mut self, ctx: &Context) {
@@ -180,32 +182,97 @@ impl eframe::App for Deduct {
             });
 
         });
-        
+
         egui::SidePanel::right("proof_rules")
             .resizable(false)
             .min_width(w * 0.25)
             .max_width(w * 0.25)
             .show(ctx, |ui| {
                 containers::ScrollArea::vertical().show(ui, |ui| {                   
+                    let tint = if self.prefs.dark_mode { Color32::WHITE } else { Color32::BLACK };
+
+                    macro_rules! rule {
+                        ($ui:ident, $path:literal) => {
+                            $ui.add(
+                                egui::Image::new(egui::include_image!($path))
+                                    .tint(tint)
+                                    .fit_to_fraction(
+                                        Vec2::new(0.975, f32::INFINITY)
+                                    )
+                            );
+                        };
+                    }
+
                     ui.collapsing("Operator Shorthands", |ui| {
-                        ui.label("Negation: ~");
-                        ui.label("Conjunction: ^ or &");
-                        ui.label("Disjunction: v");
-                        ui.label("Biconditional: <->");
-                        ui.label("Conditional: ->");
-                        ui.label("Contradiction: XX or #");
-                        ui.separator();
-                        ui.label("Necessity: []");
-                        ui.label("Possibility: <>");
+                        Grid::new("shorthand_grid")
+                        .striped(true)
+                        .num_columns(2)
+                        .show(ui, |ui| {
+                            let placeholder_tt = "Can be used to validate any arbitrary sentence.\nProofs that have reached the conclusion but still contain placeholders will be flagged as incomplete.";
+
+                            ui.label("Placeholder").on_hover_text(placeholder_tt);
+                            ui.label("?").on_hover_text(placeholder_tt);
+                            ui.end_row();
+
+                            ui.label("Negation");
+                            ui.label("~");
+                            ui.end_row();
+
+                            ui.label("Conjunction");
+                            ui.label("^ or &");
+                            ui.end_row();
+
+                            ui.label("Disjunction");
+                            ui.label("v");
+                            ui.end_row();
+
+                            ui.label("Conditional");
+                            ui.label("->");
+                            ui.end_row();
+
+                            ui.label("Biconditional");
+                            ui.label("<->");
+                            ui.end_row();
+
+                            ui.label("Contradiction");
+                            ui.label("XX or #");
+                            ui.end_row();
+
+                            ui.label("Necessity");
+                            ui.label("[ ]");
+                            ui.end_row();
+
+                            ui.label("Possibility");
+                            ui.label("<>");
+                            ui.end_row();
+                        });
                     });
 
                     ui.separator();
-                    ui.collapsing("Basic TFL", |ui| {});
-                    ui.collapsing("Derived TFL", |ui| {});
-                    ui.collapsing("System K", |ui| {});
-                    ui.collapsing("System T", |ui| {});
-                    ui.collapsing("System S4", |ui| {});
-                    ui.collapsing("System S5", |ui| {});
+
+                    ui.collapsing("Basic TFL", |ui| {
+                        rule!(ui, "static/rules/TFL.png");
+                    });
+
+                    ui.collapsing("Derived TFL", |ui| {
+                        rule!(ui, "static/rules/TFLD.png");
+                    });
+
+                    ui.collapsing("System K", |ui| {
+                        rule!(ui, "static/rules/K.png");
+                    });
+
+                    ui.collapsing("System T", |ui| {
+                        rule!(ui, "static/rules/RT.png");
+                    });
+
+                    ui.collapsing("System S4", |ui| {
+                        rule!(ui, "static/rules/R4.png");
+                    });
+
+                    ui.collapsing("System S5", |ui| {
+                        rule!(ui, "static/rules/R5.png");
+                    });
                 });
         });
 
@@ -349,7 +416,7 @@ fn fonts_init(cc: &eframe::CreationContext<'_>) {
 
     fonts.font_data.insert(
         "math".to_owned(),
-        FontData::from_static( include_bytes!("../static/latinmodern-math.otf") )
+        FontData::from_static( include_bytes!("static/latinmodern-math.otf") )
     );
 
     fonts.families.insert(
diff --git a/src/static/latinmodern-math.otf b/src/ui/static/latinmodern-math.otf
similarity index 100%
rename from src/static/latinmodern-math.otf
rename to src/ui/static/latinmodern-math.otf
diff --git a/src/ui/static/rules/.gitignore b/src/ui/static/rules/.gitignore
new file mode 100644
index 0000000..e0623f9
--- /dev/null
+++ b/src/ui/static/rules/.gitignore
@@ -0,0 +1,3 @@
+*.aux
+*.out
+*.log
\ No newline at end of file
diff --git a/src/ui/static/rules/K.png b/src/ui/static/rules/K.png
new file mode 100644
index 0000000..104c08d
Binary files /dev/null and b/src/ui/static/rules/K.png differ
diff --git a/src/ui/static/rules/Makefile b/src/ui/static/rules/Makefile
new file mode 100644
index 0000000..44dc243
--- /dev/null
+++ b/src/ui/static/rules/Makefile
@@ -0,0 +1,18 @@
+.PRECIOUS: %.tex
+
+objects := $(patsubst texf/%.texf,%.svg,$(wildcard texf/*.texf))
+
+all: $(objects)
+	sed -i 's/rgb(0%, 0%, 0%)/rgb(100%, 100%, 100%)/g' *.svg
+
+%.tex: texf/%.texf texf/rule-template.tex forallxyyc.sty
+	pandoc -f latex -t latex --template texf/rule-template.tex -o $@ $<
+
+%.pdf: %.tex
+	pdflatex $*
+
+%.svg: %.pdf
+	pdf2svg $< $@
+
+clean:
+	rm -f *.tex *.pdf *.aux *.out *.log
diff --git a/src/ui/static/rules/R4.png b/src/ui/static/rules/R4.png
new file mode 100644
index 0000000..626ea7e
Binary files /dev/null and b/src/ui/static/rules/R4.png differ
diff --git a/src/ui/static/rules/R5.png b/src/ui/static/rules/R5.png
new file mode 100644
index 0000000..3450351
Binary files /dev/null and b/src/ui/static/rules/R5.png differ
diff --git a/src/ui/static/rules/RT.png b/src/ui/static/rules/RT.png
new file mode 100644
index 0000000..a47ae25
Binary files /dev/null and b/src/ui/static/rules/RT.png differ
diff --git a/src/ui/static/rules/TFL.png b/src/ui/static/rules/TFL.png
new file mode 100644
index 0000000..7df19aa
Binary files /dev/null and b/src/ui/static/rules/TFL.png differ
diff --git a/src/ui/static/rules/TFLD.png b/src/ui/static/rules/TFLD.png
new file mode 100644
index 0000000..cd61fba
Binary files /dev/null and b/src/ui/static/rules/TFLD.png differ
diff --git a/src/ui/static/rules/forallxyyc.sty b/src/ui/static/rules/forallxyyc.sty
new file mode 100644
index 0000000..18f80b9
--- /dev/null
+++ b/src/ui/static/rules/forallxyyc.sty
@@ -0,0 +1,537 @@
+%!TEX root = forallxyyc.tex
+\NeedsTeXFormat{LaTeX2e}
+\ProvidesPackage{forallxyyc}[2011/10/29 support for a logic textbook]
+\RequirePackage{amssymb,amsmath,hyperref,multicol,ifthen,graphicx,pifont,rotating,xcolor}
+%RZ: typefaces 
+
+\usepackage[sfdefault]{universalis}
+\usepackage[osf]{Baskervaldx} % oldstyle figures
+\usepackage[bigdelims,baskervaldx]{newtxmath} 
+\usepackage[cal=boondoxo]{mathalfa}
+
+%RZ: Make sure we have a copyright symbol
+
+
+
+% The original forallx.sty was written in 2005
+% Comments marked "TB" are additions by Tim Button in September 2012
+
+%    ****************************************
+%    *            LOGICAL SYMBOLS           *
+%    ****************************************
+%
+% There are, of course, many different symbols used for the truth-functional
+% connectives. In order to make the book adaptable, the symbols are defined
+% here in the style sheet and these commands are used throughout the book.
+% To change conjunction from the ampersand to the carat, for instance,
+% change the definition of \eand from ~\&~ to \wedge. To change negation from
+% the hoe to the swung dash, change \enot from \neg to {\sim}. Other examples
+% are given below.
+%
+\def\therefore{\ensuremath{\mathrel{\ldotp\dot{}\,\ldotp}}}
+% disjunction
+\def\eor{\ensuremath{\vee}}
+% conjunction: 
+% {\,^{_{_{_{_{\mbox{\footnotesize\textbullet}}}}}}} gives the dot
+\def\eand{\ensuremath{\wedge}}
+% conditional: \supset gives the horseshoe
+\def\eif{\ensuremath{\rightarrow}}
+% biconditional: \equiv gives the triple bar
+\def\eiff{\ensuremath{\leftrightarrow}}
+% negation: {\sim} gives the swung dash 
+\def\enot{\ensuremath{\neg}}
+\def\ered{\ensuremath{\bot}}% TB: added to give an absurdity sign
+\def\maththe{\rotatebox[origin=c]{180}{$\iota$}} % TB: added to give definite description operator
+\def\proves{\ensuremath{\vdash}}
+\def\entails{\ensuremath{\vDash}}
+\def\nproves{\ensuremath{\nvdash}}
+\def\nentails{\ensuremath{\nvDash}}
+%    ****************************************
+%    *       SYMBOLS AND SCRIPTY BITS       *
+%    ****************************************
+% equivalent to commenting something out, but usable on multiple lines
+\providecommand{\nix}[1]{}
+
+\newcommand*{\script}[1]{\ensuremath{\mathcal{#1}}}
+\newcommand*{\meta}[1]{\ensuremath{\mathcal{#1}}} % TB: used for all metavariables
+% create a blank
+\newcommand*{\blank}{\underline{\hspace*{2.5em}}}
+\newcommand*{\gap}[1]{\blank$_{#1}$} % TB: used for keys, to avoid use/mention confusion
+
+% These are included for discussing formal semantics in predicate logic.
+\newcommand*{\model}[1]{\ensuremath{\mathbb{#1}}}
+\newcommand*{\extension}[1]{\ensuremath{\mbox{extension}(#1)}}
+\newcommand*{\referent}[1]{\ensuremath{\mbox{referent}(#1)}}
+  % I personally dislike the default LaTeX angle brackets. I think that
+  % they are too narrow. If you want to use them, though, you can
+  % replace < and > in the commands below with \langle and \rangle
+\newcommand*{\openntuple}{\langle}
+\newcommand*{\closentuple}{\rangle}
+\newcommand*{\ntuple}[1]{\ensuremath{\mathopen{\openntuple}}#1\ensuremath{\mathclose{\closentuple}}} 
+
+
+
+
+%    ****************************************
+%    *                PROOFS                *
+%    ****************************************
+
+% based on fitch.sty by Peter Selinger, University of Ottawa
+% v 0.4, (C) 2002 Peter Selinger
+% revised 2003--5 by P.D. Magnus
+
+% Selinger released this code under the GNU General Public License,
+% version 2 or later. So this bit of the style is free to you under
+% the GPL.
+
+% ----------------------------------------------------------------------
+% The comments in this file are intended for programmers who
+% might want to hack this package. For information on how to use the
+% package, the file fitchdoc.tex is a better place to look.
+% ----------------------------------------------------------------------
+
+% Global identifiers defined by this package start with '\nd*'. The
+% only exceptions are \ndref, \nddim, and the "nd" and "ndresume"
+% latex environments.
+
+{\chardef\x=\catcode`\*
+\catcode`\*=11
+\global\let\nd*astcode\x}
+\catcode`\*=11
+
+% The macros provided by this package mix TeX and LaTeX primitives.
+% LaTeX is used for \rule, \settowidth, \addtolength, \hspace...
+% All macros are assumed to be called in math mode.
+
+% Translation proceeds through several layers of macros. Each layer
+% consist of macros which expand into macros of the previous
+% layer. Each layer may have some global state and initialization
+% functions. Only the topmost layer (layer C) is directly
+% user-accessible. 
+
+
+% References
+
+% We start with some macros to facilitate automatic line numbering, and
+% for referencing of lines by labels. The macros defined here are:
+% \nd*reset to reset the line number count. \nd*num{x}, to generate the next
+% line number and store it in reference x; \nd*ref{x} to print the line
+% number referenced by x, \ndref{xxx} to parse a list of references,
+% separated by commas, periods, and hyphens, and translate all references to
+% line numbers. Note: \ndref ignores spaces in its argument, but puts
+% a space after each comma or period in the output. Also note: \nd*ref can be
+% useful outside a natded environment, and thus it has a user
+% accessible name. Most general ``line numbers'' actually consist of a
+% name (such as ``n'') and a number (such as ``2''), to produce output
+% such as $n+2$. \nd*set{n}{m} is called to set the letter to n and
+% the number to m. As special cases, if the second argument is empty,
+% it is not set, and if the first argument is \relax, it is not set.
+
+% Example for references:
+
+% \nd*reset \nd*num{x}; \nd*num{y}; \nd*numopt{n+1}{z}; \nd*num{zz}; 
+% \nd*ref{y}; \ndref{x, y-zz, z}
+% will produce: 1; 2; n+1; 3; 2; 1, 2-3, n+1
+
+\newcount\nd*ctr
+\def\nd*render{\expandafter\ifx\expandafter\nd*x\nd*base\nd*x\the\nd*ctr\else\nd*base\ifnum\nd*ctr<0\the\nd*ctr\else\ifnum\nd*ctr>0+\the\nd*ctr\fi\fi\fi}
+\expandafter\def\csname nd*-\endcsname{}
+
+%\def\nd*num#1{\global\advance\nd*ctr1\nd*numo{\the\nd*ctr}{#1}}
+\def\nd*num#1{\nd*numo{\nd*render}{#1}\global\advance\nd*ctr1}
+\def\nd*numopt#1#2{\nd*numo{$#1$}{#2}}
+\def\nd*numo#1#2{\edef\x{#1}\mbox{$\x$}\expandafter\global\expandafter\let\csname nd*-#2\endcsname\x}
+\def\nd*ref#1{\expandafter\let\expandafter\x\csname nd*-#1\endcsname\ifx\x\relax%
+  \errmessage{Undefined natdeduction reference: #1}\else\mbox{$\x$}\fi}
+\def\nd*noop{}
+\def\nd*set#1#2{\ifx\relax#1\nd*noop\else\global\def\nd*base{#1}\fi\ifx\relax#2\relax\else\global\nd*ctr=#2\fi}
+\def\nd*reset{\nd*set{}{1}}
+\def\nd*refa#1{\nd*ref{#1}}
+\def\nd*aux#1#2{\ifx#2-\nd*refa{#1}--\def\c{\nd*aux{}}%
+  \else\ifx#2,\nd*refa{#1}, \def\c{\nd*aux{}}%
+  \else\ifx#2;\nd*refa{#1}; \def\c{\nd*aux{}}%
+  \else\ifx#2.\nd*refa{#1}. \def\c{\nd*aux{}}%
+  \else\ifx#2)\nd*refa{#1})\def\c{\nd*aux{}}%
+  \else\ifx#2(\nd*refa{#1}(\def\c{\nd*aux{}}%
+  \else\ifx#2\nd*end\nd*refa{#1}\def\c{}%
+  \else\def\c{\nd*aux{#1#2}}%
+  \fi\fi\fi\fi\fi\fi\fi\c}
+\def\ndref#1{\nd*aux{}#1\nd*end}
+
+
+% Layer A
+
+% Layer A provides primitive picture elements which can be combined
+% into natural deduction derivations. These are: \nd*t to make a
+% topmost vertical line segment; \nd*v to make a continuation vertical
+% line segment, \nd*i to produce the indentation for a subproof,
+% \nd*s to produce the horizontal space between a vertical line and a
+% formula, \nd*u{x} to underline x with appropriate spacing for a
+% hypothesis. \nd*f{x} typesets the formula x with the appropriate vertical
+% spacing. \nd*g{x} is like \nd*i, except it puts a guard in the
+% space it creates. These elements are spaced so that they are appropriate
+% as left-aligned array entries. Line numberings and justifications
+% must be provided manually in this layer. All explicit spacing
+% information is contained in this layer; higher layers manipulate only
+% layer A primitives.
+
+% define various dimensions (explained in fitchdoc.tex):
+\newlength{\nd*dim} 
+\newdimen\nd*depthdim
+\newdimen\nd*hsep
+% user command to redefine dimensions
+\def\nddim#1#2#3#4#5#6#7#8{\nd*depthdim=#3\relax\nd*hsep=#6\relax%
+\def\nd*height{#1}\def\nd*thickness{#8}\def\nd*initheight{#2}%
+\def\nd*indent{#5}\def\nd*labelsep{#4}\def\nd*justsep{#7}}
+% set initial dimensions
+\nddim{4.5ex}{3.5ex}{1.5ex}{1em}{1.6em}{.5em}{2.5em}{.2mm}
+
+\def\nd*v{\rule[-\nd*depthdim]{\nd*thickness}{\nd*height}}
+\def\nd*t{\rule[-\nd*depthdim]{0mm}{\nd*height}\rule[-\nd*depthdim]{\nd*thickness}{\nd*initheight}}
+\def\nd*i{\hspace{\nd*indent}} 
+\def\nd*s{\hspace{\nd*hsep}}
+\def\nd*g#1{\nd*f{\makebox[\nd*indent][c]{$#1$}}}
+\def\nd*f#1{\raisebox{0pt}[0pt][0pt]{$#1$}}
+\def\nd*u#1{\makebox[0pt][l]{\settowidth{\nd*dim}{\nd*f{#1}}%
+    \addtolength{\nd*dim}{2\nd*hsep}\hspace{-\nd*hsep}\rule[-\nd*depthdim]{\nd*dim}{\nd*thickness}}\nd*f{#1}}
+
+% Example of a derivation using layer A syntax:
+
+%\begin{array}{lll}
+%  1  &  \nd*t\nd*s\nd*f            {P\vee Q}                           \\
+%  2  &  \nd*v\nd*s\nd*u            {\neg Q}                            \\
+%  3  &  \nd*v\nd*i\nd*t\nd*s\nd*u  {P}                                 \\
+%  4  &  \nd*v\nd*i\nd*v\nd*s\nd*f  {P}       &  \mbox{by 3}            \\
+%  5  &  \nd*v\nd*i\nd*t\nd*s\nd*u  {Q}                                 \\
+%  6  &  \nd*v\nd*i\nd*v\nd*s\nd*f  {\neg Q}  &  \mbox{by 2}            \\
+%  7  &  \nd*v\nd*i\nd*v\nd*s\nd*f  {\bot}    &  \mbox{by 5, 6}         \\
+%  8  &  \nd*v\nd*i\nd*v\nd*s\nd*f  {P}       &  \mbox{by 7}            \\
+%  9  &  \nd*v\nd*s\nd*f            {P}       &  \mbox{by 1, 3-4, 5-8}  \\
+%\end{array}
+
+
+% Lists
+
+% This is a bit of a hack. We implement linked lists as follows: a
+% list is either \nd*nil, or \nd*cons{T}{H}, where T is another list,
+% and H is some arbitrary code. Note that lists grow to the right. 
+% The following macros operate on a list that is stored in a macro
+% \list. 
+% \nd*push\list{item} pushes the item onto the list
+% \nd*pop\list{item} pops and discards the last item from the list
+% \nd*item\list{command} applies command to each element of the list
+% \nd*modify\list\n{elt} modifies the \n-th element of the
+% list, if there is such an element. Here \n is a counter. Elements
+% are counted from the right, starting from 1.
+
+\def\nd*push#1#2{\expandafter\gdef\expandafter#1\expandafter%
+  {\expandafter\nd*cons\expandafter{#1}{#2}}}
+\def\nd*pop#1{{\def\nd*nil{\gdef#1{\nd*nil}}\def\nd*cons##1##2%
+    {\gdef#1{##1}}#1}}
+\def\nd*iter#1#2{{\def\nd*nil{}\def\nd*cons##1##2{##1#2{##2}}#1}}
+\def\nd*modify#1#2#3{{\def\nd*nil{\gdef#1{\nd*nil}}\def\nd*cons##1##2%
+    {\advance#2-1 ##1\advance#2 1 \ifnum#2=1\nd*push#1{#3}\else%
+      \nd*push#1{##2}\fi}#1}}
+
+% we use lists of items of the forms \nd*t, \nd*v, \nd*i, and
+% \nd*g{...} to represent the current indentation level and
+% format (see Layer A, above). The following function 
+% computes the indentation for the following line by replacing all
+% items of the form \nd*t by \nd*v and \nd*g{...} by \nd*i. 
+
+\def\nd*cont#1{{\def\nd*t{\nd*v}\def\nd*v{\nd*v}\def\nd*g##1{\nd*i}%
+    \def\nd*i{\nd*i}\def\nd*nil{\gdef#1{\nd*nil}}\def\nd*cons##1##2%
+    {##1\expandafter\nd*push\expandafter#1\expandafter{##2}}#1}}
+
+% With the list syntax, a derivation can be expressed like this:
+
+% \[\begin{array}{lll}
+%   \gdef\stack{\nd*nil}
+%   \newcount\n
+%   \nd*push\stack{\nd*t}
+%   1 & \nd*iter\stack\relax\nd*s\nd*u       {\neg\exists xP(x)} \\
+%   \nd*cont\stack
+%   \nd*push\stack{\nd*i}
+%   \nd*push\stack{\nd*t}
+%   \nd*n=2\nd*modify\stack\n{\nd*g{u}}
+%   \nd*push\stack{\nd*i}
+%   \nd*push\stack{\nd*t}
+%   2 & \nd*iter\stack\relax\nd*s\nd*u       {P(u)} \\
+%   \nd*cont\stack
+%   3 & \nd*iter\stack\relax\nd*s\nd*f       {\exists xP(x)} \\
+%   \nd*cont\stack
+%   4 & \nd*iter\stack\relax\nd*s\nd*f       {\neg\exists xP(x)} \\
+%   \nd*cont\stack
+%   5 & \nd*iter\stack\relax\nd*s\nd*f       {\bot} \\
+%   \nd*cont\stack
+%   \nd*pop\stack
+%   \nd*pop\stack
+%   6 & \nd*iter\stack\relax\nd*s\nd*f       {\neg P(u)} \\
+%   \nd*cont\stack
+%   \nd*pop\stack
+%   \nd*pop\stack
+%   7 & \nd*iter\stack\relax\nd*s\nd*f       {\forall y\neg P(y)} \\
+%   \nd*cont\stack
+%  \end{array}
+% \]
+
+
+% Layer B
+
+% Layer B is simply a wrapper around layer A. It provides commands
+% \nd*beginb, \nd*resumeb, \nd*endb, \nd*openb, \nd*closeb,
+% \nd*guardb, \nd*hypob, and \nd*haveb which abstract from the layer A 
+% primitives. This includes automatic line numbering, and automatic
+% indentation. \nd*beginb and \nd*endb enclose a natural deduction in
+% layer B syntax. \nd*resumeb is like \nd*beginb, except that it
+% resumes a deduction in progress (for instance, after a manual page
+% break). \nd*openb and \nd*closeb open, respectively close, a
+% subproof.  \nd*guardb{n}{g} adds the guard g to the nth enclosing
+% subderivation (counted from 1 from the inside). \nd*hypob 
+% introduces a hypothesis, and \nd*haveb introduces a non-hypothesis
+% line in a proof.  Line numbering is integrated, but justifications
+% must still be given manually. Also, proof lines must still be
+% terminated by '\\'. An idiosyncracy of this layer is that in a list
+% of several hypotheses, all but the last one must be called with
+% \nd*haveb, not \nd*hypob, to avoid drawing a horizontal line under
+% each of them.
+
+\newcount\nd*n
+\def\nd*beginb{\begingroup\nd*reset\gdef\nd*stack{\nd*nil}\nd*push\nd*stack{\nd*t}%
+  \begin{array}{l@{\hspace{\nd*labelsep}}l@{\hspace{\nd*justsep}}l}}
+\def\nd*resumeb{\begingroup\begin{array}{r@{\hspace{\nd*labelsep}}l@{\hspace{\nd*justsep}}l}}
+\def\nd*endb{\end{array}\endgroup}
+\def\nd*hypob#1#2{\nd*f{\nd*num{#1}}&\nd*iter\nd*stack\relax\nd*cont\nd*stack\nd*s\nd*u{#2}&}
+\def\nd*haveb#1#2{\nd*f{\nd*num{#1}}&\nd*iter\nd*stack\relax\nd*cont\nd*stack\nd*s\nd*f{#2}&}
+\def\nd*openb{\nd*push\nd*stack{\nd*i}\nd*push\nd*stack{\nd*t}}
+\def\nd*closeb{\nd*pop\nd*stack\nd*pop\nd*stack}
+\def\nd*guardb#1#2{\nd*n=#1\multiply\nd*n by 2 \nd*modify\nd*stack\nd*n{\nd*g{#2}}}
+% one must first \close the outermost layer of assumption
+% it's a bit of a hack
+
+% Example of a derivation using layer B syntax. Note that the "line
+% numbers" are really labels, which will be replaced by consecutive
+% line numbers in the output.
+
+% \[
+%   \nd*beginb
+%   \nd*haveb  {1}{P\vee Q}                               \\
+%   \nd*hypob  {2}{\neg Q}                                \\
+%   \nd*openb
+%   \nd*hypob  {3}{P}                                     \\
+%   \nd*haveb  {4}{P}       \mbox{by \ndref{3}}           \\
+%   \nd*closeb
+%   \nd*openb
+%   \nd*hypob  {5}{Q}                                     \\
+%   \nd*haveb  {6}{\neg Q}  \mbox{by \ndref{2}}           \\
+%   \nd*haveb  {6a}{\bot}   \mbox{by \ndref{5,6}}         \\
+%   \nd*haveb  {6b}{P}      \mbox{by \ndref{6a}}          \\
+%   \nd*closeb
+%   \nd*haveb  {8}{P}       \mbox{by \ndref{1,3-4,5-6b}}  \\
+%   \nd*endb
+% \]
+
+% Here is another example, using a guard.
+
+% \[
+%   \nd*beginb
+%   \nd*hypob  {1}{\neg\exists xP(x)}   \\
+%   \nd*openb
+%   \nd*guardb {1}{u}
+%   \nd*openb
+%   \nd*hypob  {2}{P(u)}                \\
+%   \nd*haveb  {3}{\exists xP(x)}       \mbox{by \ndref{2}}  \\
+%   \nd*haveb  {4}{\neg\exists xP(x)}   \mbox{by \ndref{1}}  \\
+%   \nd*haveb  {5}{\bot}                \mbox{by \ndref{3,4}}\\
+%   \nd*closeb
+%   \nd*haveb  {6}{\neg P(u)}           \mbox{by \ndref{2-5}}\\
+%   \nd*closeb
+%   \nd*haveb  {7}{\forall y\neg P(y)}  \mbox{by \ndref{2-6}}\\
+%   \nd*endb
+% \]
+
+
+% Layer C
+
+% Layer C is the syntax used by the end user. It is implemented as a
+% wrapper around layer B, providing six additional conveniences: 
+% (1) no more need for explicit '\\', (2) all hypotheses 
+% are denoted \hypo, (3) a convenient syntax for writing justification
+% labels, (4) a latex environment, (5) guard as optional argument to
+% \have, \hypo, or \open, (6) optional relabeling arguments. The user
+% level commands are similar to those of layer B: they are called
+% \begin{nd}, \end{nd}, \open, \close, \hypo, \have. In addition there
+% is a \by command for writing justification labels, in the style of
+% \by{$\vee$E}{1,2-4,5-6}. For convenience, a number of abbreviations
+% is also provided, for instance \ie for \by{$\Rightarrow$E}
+% etc. These commands are only visible inside an nd-environment; thus
+% they do not interfere with the global name space. There is also an
+% environment ndresume which is like nd, except that it continues a
+% proof in progress (with continuous nesting and labeling).
+
+% The layer C macros work by storing each line in a data structure
+% \ppp,\nd*typ,\nd*byt. The line is ejected when the beginning of the next
+% line is read, and once at the very end. In this way, we can put in
+% the correct line breaks (whether or not the line carries a
+% justification), and a hypothesis does not get typeset until we know
+% whether it is followed by another hypothesis. \nd*sto stores a new
+% line, \nd*clr clears the current line, \nd*cmd outputs the current
+% line. Finally, \nd*init puts all the commands which are visible
+% inside an nd-environment in the current name space.
+
+\def\nd*clr{\gdef\nd*cmd{}}
+\def\nd*sto#1#2#3{\gdef\nd*typ{#1}\gdef\nd*byt{}%
+  \gdef\nd*cmd{\nd*typ{#2}{#3}\nd*byt\\}}
+\def\nd*hyc#1#2{\def\nd*typ{\nd*haveb}\nd*cmd\nd*sto{\nd*hypob}{#1}{#2}}
+\def\nd*hac#1#2{\nd*cmd\nd*sto{\nd*haveb}{#1}{#2}}
+%\def\nd*htc#1#2{\nd*cmd\nd*sto{\nd*theob}{#1}{#2}}
+
+% usage: \optarg{default}{continuation}xxx - reads an optional argument, 
+% supplies default if necessary, then continues with continuation. 
+% Continuation expects optional argument between [...]. I.e., 
+% \optarg{d}{c}[xxx] => c[xxx], and \optarg{d}{c}x => c[d]x if x != '['. 
+% Behavior is undefined if x is {[...}. \optargg is similar except it 
+% takes two continuations: first one for optional argument present, second 
+% for not present. It takes no default value.
+
+\def\optarg#1#2#3{\ifx[#3\def\c{#2#3}\else\def\c{#2[#1]{#3}}\fi\c}
+\def\optargg#1#2#3{\ifx[#3\def\c{#1#3}\else\def\c{#2{#3}}\fi\c}
+
+\def\nd*hyx[#1][#2]#3[#4]#5{\ifx\relax#4\relax\else\nd*guardb{1}{#4}\fi\nd*hyc{#3}{#5}\nd*set{#1}{#2}}
+\def\nd*hax[#1][#2]#3[#4]#5{\ifx\relax#4\relax\else\nd*guardb{1}{#4}\fi\nd*hac{#3}{#5}\nd*set{#1}{#2}}
+%\def\nd*htx[#1][#2]#3[#4]#5{\ifx\relax#4\relax\else\nd*guardb{1}{#4}\fi\nd*htc{#3}{#5}\nd*set{#1}{#2}}
+
+% \nd*five{\a}: read five, partly optional arguments of the shape [][]{}[]{}, 
+% then call \a with these arguments.
+\def\nd*five#1{\optargg{\nd*four{#1}}{\nd*two{#1}}}
+\def\nd*four#1[#2]{\optarg{0}{\nd*three{#1}[#2]}}
+\def\nd*three#1[#2][#3]#4{\optarg{}{#1[#2][#3]{#4}}}
+\def\nd*two#1{\nd*three{#1}[\relax][]}
+
+\def\nd*have{\nd*five{\nd*hax}}
+\def\nd*theo{\nd*five{\nd*htx}} % To be like have
+\def\nd*hypo{\nd*five{\nd*hyx}}
+\def\nd*base{undefined}
+
+\def\nd*open{\optargg{\nd*openopt}{\nd*opennoopt}}
+\def\nd*openopt[#1]{\nd*cmd\nd*clr\nd*openb\nd*guard{#1}}
+\def\nd*opennoopt#1{\nd*cmd\nd*clr\nd*openb#1}
+\def\nd*close{\nd*cmd\nd*clr\nd*closeb}
+\def\nd*guard{\optarg{1}{\nd*guardc}}
+\def\nd*guardc[#1]#2{\nd*guardb{#1}{#2}}
+
+\def\nd*by#1#2{\ifx\nd*x#2\nd*x\gdef\nd*byt{\mbox{#1}}\else\gdef\nd*byt{\mbox{#1\ \ndref{#2}}}\fi}
+
+% * * *
+% This block defines the natural deduction rules.
+% Rules designated by ordinary letters may be specified with \by{RULE}
+% * * *
+
+\def\nd*init{%
+  \let\open\nd*open%
+  \let\close\nd*close%
+  \let\hypo\nd*hypo%
+  \let\have\nd*have%
+%  \let\theo\nd*theo%
+  \let\by\nd*by%
+  \let\guard\nd*guard%
+  \def\bi{\by{{\eiff}I}}%
+  \def\be{\by{{\eiff}E}}%
+  \def\ci{\by{{\eif}I}}%
+  \def\ce{\by{{\eif}E}}%
+  \def\Ai{\by{$\forall$I}}%
+  \def\Ae{\by{$\forall$E}}%
+  \def\Ei{\by{$\exists$I}}%
+  \def\Ee{\by{$\exists$E}}%
+  \def\ae{\by{{\eand}E}}%
+  \def\ai{\by{{\eand}I}}%
+  \def\oi{\by{{\eor}I}}%
+  \def\oe{\by{{\eor}E}}%
+  \def\ni{\by{{\enot}I}}%
+  \def\ne{\by{{\enot}E}}%
+  \def\ri{\by{{\enot}E}}% RZ: this is now \enot E
+  \def\re{\by{X}}% RZ: explosion
+  \def\ii{\by{$=$I}}%
+  \def\ie{\by{$=$E}}%
+  \def\tnd{\by{LEM}}% RZ: excluded middle
+  \def\ip{\by{IP}}% RZ: indirect proof
+  \def\dne{\by{DNE}}% TB: double negation elimination (derived rule)
+  \def\mt{\by{MT}}% TB: modus tollens (derived rule)
+  \def\ds{\by{DS}}% TB: disjunctive syllogism (a derived rule in Cambridge version)
+  \def\dem{\by{DeM}}% TB: De Morgan rule (derived rule)
+  \def\cq{\by{CQ}}% TB: conversion of quantifiers (derived rule)
+}
+\newenvironment{nd}{\begingroup\nd*init\nd*beginb\nd*clr}{\nd*cmd\nd*endb\endgroup}
+\newenvironment{ndresume}{\begingroup\nd*init\nd*resumeb\nd*clr}%
+  {\nd*cmd\nd*endb\endgroup}
+
+% Example of a derivation using layer C syntax. As before, the "line
+% numbers" are really labels, which will be replaced by consecutive
+% line numbers in the output.
+
+% \[
+% \begin{nd}
+%   \hypo{1}  {P\vee Q}   
+%   \hypo{2}  {\neg Q}                         
+%   \open                              
+%   \hypo{3a} {P}
+%   \have{3b} {P}        \r{3a}
+%   \close                   
+%   \open
+%   \hypo{4a} {Q}
+%   \have{4b} {\neg Q}   \r{2}
+%   \have{4c} {\bot}     \ne{4a,4b}
+%   \have{4d} {P}        \be{4c}
+%   \close                             
+%   \have{5}  {P}        \oe{1,3a-3b,4a-4d}                 
+% \end{nd}
+% \]
+
+% Another example of layer C syntax, using guards and relabelings:
+
+% \begin{nd}
+%   \hypo          {1} {P\vee Q}
+%   \open
+%   \hypo          {2}[u] {P}
+%   \have [\vdots] {3} {\vdots}
+%   \have [n][-1]  {4} {A\wedge B}
+%   \close
+%   \open
+%   \hypo          {5} {Q}
+%   \have [\vdots] {6} {\vdots}
+%   \have [m]      {7} {A\wedge B}
+%   \close
+%   \have          {8} {A\wedge B}  \oe{1,2-(4),5-7}
+%   \have [\vdots] {9} {\vdots}
+%   \have [][100] {10} {A}          \ae{8}
+% \end{nd}
+
+\catcode`\*=\nd*astcode
+
+% a command for indicating the goal in a proof or subproof
+\newcommand*{\want}[1]{\by{want \ensuremath{#1}}{}}
+% an environment that separates the proof from surrounding paragraphs
+\newenvironment{proof}
+	{\begin{list}{}{}\item$\begin{nd}}
+	{\end{nd}$\end{list}}
+
+% I keep mixing up the \ce and \ae commands, so I define a less ambiguous
+% alternate set of commands
+
+\newcommand*{\notI}{\ni}
+\newcommand*{\notE}{\ne}
+\newcommand*{\iffI}{\bi}
+\newcommand*{\iffE}{\be}
+\newcommand*{\ifI}{\ci}
+\newcommand*{\ifE}{\ce}
+\newcommand*{\andI}{\ai}
+\newcommand*{\andE}{\ae}
+\newcommand*{\orI}{\oi}
+\newcommand*{\orE}{\oe}
+\newcommand*{\forallI}{\Ai}
+\newcommand*{\forallE}{\Ae}
+\newcommand*{\existsI}{\Ei}
+\newcommand*{\existsE}{\Ee}
+
+
+
diff --git a/src/ui/static/rules/texf/FOL/Ae.texf b/src/ui/static/rules/texf/FOL/Ae.texf
new file mode 100644
index 0000000..3571f5a
--- /dev/null
+++ b/src/ui/static/rules/texf/FOL/Ae.texf
@@ -0,0 +1,4 @@
+$\begin{nd}
+    \have[m]{a}{\forall \meta{x}\meta{A}(\ldots \meta{x} \ldots \meta{x}\ldots)}
+	\have[\ ]{c}{\meta{A}(\ldots \meta{c} \ldots \meta{c}\ldots)} \Ae{a}
+\end{nd}$
diff --git a/src/ui/static/rules/texf/FOL/Ai.texf b/src/ui/static/rules/texf/FOL/Ai.texf
new file mode 100644
index 0000000..af6f886
--- /dev/null
+++ b/src/ui/static/rules/texf/FOL/Ai.texf
@@ -0,0 +1,4 @@
+$\begin{nd}
+    \have[m]{a}{\meta{A}(\ldots \meta{c} \ldots \meta{c}\ldots)}
+	\have[\ ]{c}{\forall \meta{x}\meta{A}(\ldots \meta{x} \ldots \meta{x}\ldots)} \Ai{a}
+\end{nd}$
diff --git a/src/ui/static/rules/texf/FOL/Ee.texf b/src/ui/static/rules/texf/FOL/Ee.texf
new file mode 100644
index 0000000..17363cb
--- /dev/null
+++ b/src/ui/static/rules/texf/FOL/Ee.texf
@@ -0,0 +1,8 @@
+$\begin{nd}
+	\have[m]{a}{\exists \meta{x}\meta{A}(\ldots \meta{x} \ldots \meta{x}\ldots)}
+	\open	
+		\hypo[i]{b}{\meta{A}(\ldots \meta{c} \ldots \meta{c}\ldots)}
+		\have[j]{c}{\meta{B}}
+	\close
+	\have[\ ]{d}{\meta{B}} \Ee{a,b-c}
+\end{nd}$
diff --git a/src/ui/static/rules/texf/FOL/Ei.texf b/src/ui/static/rules/texf/FOL/Ei.texf
new file mode 100644
index 0000000..2055d0b
--- /dev/null
+++ b/src/ui/static/rules/texf/FOL/Ei.texf
@@ -0,0 +1,4 @@
+$\begin{nd}
+	\have[m]{a}{\meta{A}(\ldots \meta{c} \ldots \meta{c}\ldots)}
+	\have[\ ]{c}{\exists \meta{x}\meta{A}(\ldots \meta{x} \ldots \meta{c}\ldots)} \Ei{a}
+\end{nd}$
diff --git a/src/ui/static/rules/texf/FOL/Ie.texf b/src/ui/static/rules/texf/FOL/Ie.texf
new file mode 100644
index 0000000..0fb2d2c
--- /dev/null
+++ b/src/ui/static/rules/texf/FOL/Ie.texf
@@ -0,0 +1,9 @@
+$\begin{nd}
+  \have[m]{e}{\meta{a}=\meta{b}}
+	\have[n]{a}{\meta{A}(\ldots \meta{a} \ldots \meta{a}\ldots)}
+	\have[\ ]{ea1}{\meta{A}(\ldots \meta{b} \ldots \meta{a}\ldots)} \by{=E}{e,a}
+
+	\have[m]{e}{\meta{a}=\meta{b}}
+\\	\have[n]{a}{\meta{A}(\ldots \meta{b} \ldots \meta{b}\ldots)}
+	\have[\ ]{ea2}{\meta{A}(\ldots \meta{a} \ldots \meta{b}\ldots)} \by{=E}{e,a}
+\end{nd}$
diff --git a/src/ui/static/rules/texf/FOL/Ii.texf b/src/ui/static/rules/texf/FOL/Ii.texf
new file mode 100644
index 0000000..b0b35bd
--- /dev/null
+++ b/src/ui/static/rules/texf/FOL/Ii.texf
@@ -0,0 +1,3 @@
+$\begin{nd}
+	\have[\ \,\,\,]{x}{\meta{c}=\meta{c}} \by{=I}{}
+\end{nd}$
diff --git a/src/ui/static/rules/texf/K.texf b/src/ui/static/rules/texf/K.texf
new file mode 100644
index 0000000..eba2af7
--- /dev/null
+++ b/src/ui/static/rules/texf/K.texf
@@ -0,0 +1,31 @@
+$\begin{nd}
+\open
+	\hypo[i]{a}{\Box}
+	\have[j]{nb}{\meta{A}}
+\close
+\have[\hskip .8em]{na}{\Box\meta{A}}\by{$\Box$I}{a-nb}
+
+\have[i]{ab}{\Box\meta{A}}
+\\\open
+	\hypo[ ]{a}{\Box}
+	\have[j]{nb}{\meta{A}}\by{$\Box$E}{ab}
+\close
+
+	\have[m]{ab}{\enot \Box \enot \meta{A}}
+\\	\have[\ ]{dm}{\Diamond \meta{A}}\by{Def $\Diamond$}{ab}
+
+	\have[m]{ab}{\Diamond \meta{A}}
+\\	\have[\ ]{dm}{\enot \Box \enot \meta{A}}\by{Def $\Diamond$}{ab}
+
+	\have[m]{ab}{\enot \Box \meta{A}}
+\\	\have[\ ]{dm}{\Diamond \enot \meta{A}}\by{MC}{ab}
+
+	\have[m]{ab}{\Diamond \enot \meta{A}}
+\\	\have[\ ]{dm}{\enot \Box \meta{A}}\by{MC}{ab}
+
+	\have[m]{ab}{\enot \Diamond \meta{A}}
+\\	\have[\ ]{dm}{\Box \enot \meta{A}}\by{MC}{ab}
+
+	\have[m]{ab}{\Box \enot \meta{A}}
+\\	\have[\ ]{dm}{\enot \Diamond \meta{A}}\by{MC}{ab}
+\end{nd}$
\ No newline at end of file
diff --git a/src/ui/static/rules/texf/R4.texf b/src/ui/static/rules/texf/R4.texf
new file mode 100644
index 0000000..d720a7a
--- /dev/null
+++ b/src/ui/static/rules/texf/R4.texf
@@ -0,0 +1,7 @@
+$\begin{nd}
+\have[i]{ab}{\Box\meta{A}}
+\open
+	\hypo[ ]{a}{\Box}
+	\have[j]{nb}{\Box \meta{A}}\by{R4}{ab}
+\close
+\end{nd}$
diff --git a/src/ui/static/rules/texf/R5.texf b/src/ui/static/rules/texf/R5.texf
new file mode 100644
index 0000000..a4b9fbe
--- /dev/null
+++ b/src/ui/static/rules/texf/R5.texf
@@ -0,0 +1,7 @@
+$\begin{nd}
+\have[i]{ab}{\enot \Box\meta{A}}
+\open
+	\hypo[ ]{a}{\Box}
+	\have[j]{nb}{\enot \Box \meta{A}}\by{R5}{ab}
+\close
+\end{nd}$
diff --git a/src/ui/static/rules/texf/RT.texf b/src/ui/static/rules/texf/RT.texf
new file mode 100644
index 0000000..0c2e166
--- /dev/null
+++ b/src/ui/static/rules/texf/RT.texf
@@ -0,0 +1,5 @@
+$\begin{nd}
+	\have[m]{ab}{\Box \meta{A}}
+	\have[\ ]{a}{\meta{A}} \by{RT}{ab}
+\end{nd}$
+
diff --git a/src/ui/static/rules/texf/TFL.texf b/src/ui/static/rules/texf/TFL.texf
new file mode 100644
index 0000000..ffa4472
--- /dev/null
+++ b/src/ui/static/rules/texf/TFL.texf
@@ -0,0 +1,79 @@
+$\begin{nd}
+	\have[m]{a}{\meta{A}}
+	\have[\ ]{c}{\meta{A}} \by{R}{a}
+
+	\have[m]{a}{\meta{A}}
+\\	\have[n]{b}{\meta{B}}
+	\have[\ ]{c}{\meta{A}\eand\meta{B}} \ai{a, b}
+
+	\have[m]{ab}{\meta{A}\eand\meta{B}}
+\\	\have[\ ]{a}{\meta{A}} \ae{ab}
+
+	\have[m]{ab}{\meta{A}\eand\meta{B}}
+\\	\have[\ ]{b}{\meta{B}} \ae{ab}
+
+	\have[m]{a}{\meta{A}}
+\\	\have[\ ]{ab}{\meta{A}\eor\meta{B}}\oi{a}
+
+	\have[m]{a}{\meta{A}}
+\\	\have[\ ]{ba}{\meta{B}\eor\meta{A}}\oi{a}
+
+	\have[m]{ab}{\meta{A}\eor\meta{B}}
+\\	\open
+		\hypo[i]{a}{\meta{A}}
+		\have[j]{c1}{\meta{C}}
+	\close
+	\open
+		\hypo[k]{b}{\meta{B}}
+		\have[l]{c2}{\meta{C}}
+	\close
+	\have[\ ]{c}{\meta{C}} \oe{ab,a-c1, b-c2}
+
+\open
+		\hypo[i]{a}{\meta{A}}
+		\have[j]{b}{\meta{B}}
+\close
+\have[\hskip .8em]{ab}{\meta{A}\eif\meta{B}}\ci{a-b}
+
+	\have[m]{ab}{\meta{A}\eif\meta{B}}
+\\	\have[n]{a}{\meta{A}}
+	\have[\ ]{b}{\meta{B}} \ce{ab,a}
+
+\open
+	\hypo[i]{a1}{\meta{A}} 
+\\	\have[j]{b1}{\meta{B}}
+\close
+\open
+	\hypo[k]{b2}{\meta{B}}
+	\have[l]{a2}{\meta{A}}
+\close
+\have[\hskip .8em]{ab}{\meta{A}\eiff\meta{B}}\bi{a1-b1,b2-a2}
+
+	\have[m]{ab}{\meta{A}\eiff\meta{B}}
+\\	\have[n]{a}{\meta{A}}
+	\have[\ ]{b}{\meta{B}} \be{ab,a}
+
+	\have[m]{ab}{\meta{A}\eiff\meta{B}}
+\\	\have[n]{a}{\meta{B}}
+	\have[\ ]{b}{\meta{A}} \be{ab,a}
+
+\open
+	\hypo[i]{a}{\meta{A}}
+\\	\have[j]{nb}{\ered}
+\close
+\have[\hskip .8em]{na}{\enot\meta{A}}\ni{a-nb}
+
+\have[m]{na}{\enot\meta{A}}
+\\ \have[n]{a}{\meta{A}}
+\have[ ]{bot}{\ered}\ri{na, a}
+
+   \have[m]{bot}{\ered}
+\\ \have[ ]{}{\meta{A}}\re{bot}
+
+\open
+	\hypo[i]{a}{\enot\meta{A}}
+\\	\have[j]{nb}{\ered}
+\close
+\have[\hskip .8em]{na}{\meta{A}}\ip{a-nb}
+\end{nd}$
+
diff --git a/src/ui/static/rules/texf/TFLD.texf b/src/ui/static/rules/texf/TFLD.texf
new file mode 100644
index 0000000..36a53ca
--- /dev/null
+++ b/src/ui/static/rules/texf/TFLD.texf
@@ -0,0 +1,38 @@
+$\begin{nd}
+	\have[m]{ab}{\meta{A} \eor \meta{B}}
+	\have[n]{nb}{\enot \meta{A}}
+	\have[\ ]{con}{\meta{B}}\by{DS}{ab, nb}
+
+	\have[m]{ab}{\meta{A} \eor \meta{B}}
+\\	\have[n]{nb}{\enot \meta{B}}
+	\have[\ ]{con}{\meta{A}}\by{DS}{ab, nb}
+
+    \have[m]{ab}{\meta{A}\eif\meta{B}}
+\\  \have[n]{a}{\enot\meta{B}}
+    \have[\ ]{b}{\enot\meta{A}} \by{MT}{ab,a}
+
+    \have[m]{dna}{\enot \enot \meta{A}}
+\\  \have[ ]{a}{\meta{A}}\dne{dna}
+
+    \open
+	  \hypo[i]{a}{\meta{A}}
+\\	  \have[j]{c1}{\meta{B}}
+    \close
+    \open
+	  \hypo[k]{b}{\enot\meta{A}}
+	  \have[l]{c2}{\meta{B}}
+    \close
+    \have[\hskip .8em]{ab}{\meta{B}}\tnd{a-c1,b-c2}
+
+	\have[m]{ab}{\enot (\meta{A} \eor \meta{B})}
+\\	\have[\ ]{dm}{\enot \meta{A} \eand \enot \meta{B}}\dem{ab}
+
+	\have[m]{ab}{\enot \meta{A} \eand \enot \meta{B}}
+\\	\have[\ ]{dm}{\enot (\meta{A} \eor \meta{B})}\dem{ab}
+
+	\have[m]{ab}{\enot (\meta{A} \eand \meta{B})}
+\\	\have[\ ]{dm}{\enot \meta{A} \eor \enot \meta{B}}\dem{ab}
+
+	\have[m]{ab}{\enot \meta{A} \eor \enot \meta{B}}
+\\	\have[\ ]{dm}{\enot (\meta{A} \eand \meta{B})}\dem{ab}
+\end{nd}$
\ No newline at end of file
diff --git a/src/ui/static/rules/texf/rule-template.tex b/src/ui/static/rules/texf/rule-template.tex
new file mode 100644
index 0000000..ab6ff2e
--- /dev/null
+++ b/src/ui/static/rules/texf/rule-template.tex
@@ -0,0 +1,6 @@
+\documentclass[12pt]{standalone}
+\usepackage{forallxyyc}
+
+\begin{document}
+$body$
+\end{document}