diff --git a/index.html b/index.html
index 260db32d..a9761657 100644
--- a/index.html
+++ b/index.html
@@ -5,20 +5,20 @@
     <meta charset="utf-8" />
     <title>Aris</title>
     <!-- integrity="sha384-9aIt2nRpC12Uk9gS9baDl411NQApFmC26EwAOH8WgZl5MYYxFfc+NcPb1dKGj7Sk"  -->
-    <link rel="stylesheet" href="vendored/bootstrap.min.css" crossorigin="anonymous">
+    <link rel="stylesheet" href="vendored/bootstrap.min.css" integrity="sha384-9aIt2nRpC12Uk9gS9baDl411NQApFmC26EwAOH8WgZl5MYYxFfc+NcPb1dKGj7Sk" crossorigin="anonymous">
     <!-- integrity="sha384-rsfqTKW9hzXAJ0B/Q1jIAG4SToclKWD9BrQv7uaaw5KlkLVsOWRb0SOXq4uVnBYA"  -->
-    <link rel="stylesheet" href="vendored/bootstrap-submenu.min.css" crossorigin="anonymous">
+    <link rel="stylesheet" href="vendored/bootstrap-submenu.min.css" integrity="sha384-rsfqTKW9hzXAJ0B/Q1jIAG4SToclKWD9BrQv7uaaw5KlkLVsOWRb0SOXq4uVnBYA" crossorigin="anonymous">
     <link rel="stylesheet" href="styles.css">
     <link rel="stylesheet" href="dark-theme.css">
 </head>
 
 <body>
     <!-- integrity="sha384-KJ3o2DKtIkvYIK3UENzmM7KCkRr/rE9/Qpg6aAZGJwFDMVNA/GpGFF93hXpG5KkN" -->
-    <script src="vendored/jquery-3.2.1.slim.min.js" crossorigin="anonymous"></script>
+    <script src="vendored/jquery-3.2.1.slim.min.js" integrity="sha384-KJ3o2DKtIkvYIK3UENzmM7KCkRr/rE9/Qpg6aAZGJwFDMVNA/GpGFF93hXpG5KkN" crossorigin="anonymous"></script>
     <!-- integrity="sha384-1CmrxMRARb6aLqgBO7yyAxTOQE2AKb9GfXnEo760AUcUmFx3ibVJJAzGytlQcNXd" -->
-    <script src="vendored/bootstrap.bundle.min.js" crossorigin="anonymous"></script>
+    <script src="vendored/bootstrap.bundle.min.js" integrity="sha384-1CmrxMRARb6aLqgBO7yyAxTOQE2AKb9GfXnEo760AUcUmFx3ibVJJAzGytlQcNXd" crossorigin="anonymous"></script>
     <!-- integrity="sha384-p9cpfn4GxrhaxjNJV0HguYSwg/S0x5a3tLXFMyBQtrGd0zdVWRKwpqNGuNRrfLtH" -->
-    <script src="vendored/bootstrap-submenu.min.js" crossorigin="anonymous"></script>
+    <script src="vendored/bootstrap-submenu.min.js" integrity="sha384-p9cpfn4GxrhaxjNJV0HguYSwg/S0x5a3tLXFMyBQtrGd0zdVWRKwpqNGuNRrfLtH" crossorigin="anonymous"></script>
     <script>
         // Close Bootstrap popovers by clicking outside of them
         //
diff --git a/pkg/aris_web_app.d.ts b/pkg/aris_web_app.d.ts
index b4c19b50..df8ff218 100644
--- a/pkg/aris_web_app.d.ts
+++ b/pkg/aris_web_app.d.ts
@@ -11,11 +11,11 @@ export interface InitOutput {
   readonly __wbindgen_realloc: (a: number, b: number, c: number, d: number) => number;
   readonly __wbindgen_export_2: WebAssembly.Table;
   readonly __wbindgen_export_3: WebAssembly.Table;
-  readonly closure269_externref_shim: (a: number, b: number, c: number) => void;
-  readonly _dyn_core__ops__function__FnMut_____Output___R_as_wasm_bindgen__closure__WasmClosure___describe__invoke__ha8a700ca1b2368f1: (a: number, b: number) => void;
-  readonly closure276_externref_shim: (a: number, b: number, c: number) => void;
-  readonly closure579_externref_shim: (a: number, b: number, c: number) => void;
-  readonly closure652_externref_shim: (a: number, b: number, c: number) => void;
+  readonly closure405_externref_shim: (a: number, b: number, c: number) => void;
+  readonly _dyn_core__ops__function__FnMut_____Output___R_as_wasm_bindgen__closure__WasmClosure___describe__invoke__had26f60e34ffd4b2: (a: number, b: number) => void;
+  readonly closure412_externref_shim: (a: number, b: number, c: number) => void;
+  readonly closure575_externref_shim: (a: number, b: number, c: number) => void;
+  readonly closure647_externref_shim: (a: number, b: number, c: number) => void;
   readonly __wbindgen_free: (a: number, b: number, c: number) => void;
   readonly __wbindgen_exn_store: (a: number) => void;
   readonly __externref_table_alloc: () => number;
diff --git a/pkg/aris_web_app.js b/pkg/aris_web_app.js
index 3f47b28a..22680f57 100644
--- a/pkg/aris_web_app.js
+++ b/pkg/aris_web_app.js
@@ -183,23 +183,23 @@ function makeMutClosure(arg0, arg1, dtor, f) {
     return real;
 }
 function __wbg_adapter_22(arg0, arg1, arg2) {
-    wasm.closure269_externref_shim(arg0, arg1, arg2);
+    wasm.closure405_externref_shim(arg0, arg1, arg2);
 }
 
 function __wbg_adapter_25(arg0, arg1) {
-    wasm._dyn_core__ops__function__FnMut_____Output___R_as_wasm_bindgen__closure__WasmClosure___describe__invoke__ha8a700ca1b2368f1(arg0, arg1);
+    wasm._dyn_core__ops__function__FnMut_____Output___R_as_wasm_bindgen__closure__WasmClosure___describe__invoke__had26f60e34ffd4b2(arg0, arg1);
 }
 
 function __wbg_adapter_28(arg0, arg1, arg2) {
-    wasm.closure276_externref_shim(arg0, arg1, arg2);
+    wasm.closure412_externref_shim(arg0, arg1, arg2);
 }
 
 function __wbg_adapter_31(arg0, arg1, arg2) {
-    wasm.closure579_externref_shim(arg0, arg1, arg2);
+    wasm.closure575_externref_shim(arg0, arg1, arg2);
 }
 
 function __wbg_adapter_34(arg0, arg1, arg2) {
-    wasm.closure652_externref_shim(arg0, arg1, arg2);
+    wasm.closure647_externref_shim(arg0, arg1, arg2);
 }
 
 export function run_app() {
@@ -319,14 +319,14 @@ function __wbg_get_imports() {
     imports.wbg.__wbg_setcachekey_80183b7cfc421143 = function(arg0, arg1) {
         arg0.__yew_subtree_cache_key = arg1 >>> 0;
     };
+    imports.wbg.__wbg_setlistenerid_3183aae8fa5840fb = function(arg0, arg1) {
+        arg0.__yew_listener_id = arg1 >>> 0;
+    };
     imports.wbg.__wbg_listenerid_12315eee21527820 = function(arg0, arg1) {
         const ret = arg1.__yew_listener_id;
         getDataViewMemory0().setInt32(arg0 + 4 * 1, isLikeNone(ret) ? 0 : ret, true);
         getDataViewMemory0().setInt32(arg0 + 4 * 0, !isLikeNone(ret), true);
     };
-    imports.wbg.__wbg_setlistenerid_3183aae8fa5840fb = function(arg0, arg1) {
-        arg0.__yew_listener_id = arg1 >>> 0;
-    };
     imports.wbg.__wbg_new_abda76e883ba8a5f = function() {
         const ret = new Error();
         return ret;
@@ -766,24 +766,24 @@ function __wbg_get_imports() {
     imports.wbg.__wbindgen_throw = function(arg0, arg1) {
         throw new Error(getStringFromWasm0(arg0, arg1));
     };
-    imports.wbg.__wbindgen_closure_wrapper700 = function(arg0, arg1, arg2) {
-        const ret = makeMutClosure(arg0, arg1, 270, __wbg_adapter_22);
+    imports.wbg.__wbindgen_closure_wrapper1012 = function(arg0, arg1, arg2) {
+        const ret = makeMutClosure(arg0, arg1, 406, __wbg_adapter_22);
         return ret;
     };
-    imports.wbg.__wbindgen_closure_wrapper702 = function(arg0, arg1, arg2) {
-        const ret = makeMutClosure(arg0, arg1, 270, __wbg_adapter_25);
+    imports.wbg.__wbindgen_closure_wrapper1014 = function(arg0, arg1, arg2) {
+        const ret = makeMutClosure(arg0, arg1, 406, __wbg_adapter_25);
         return ret;
     };
-    imports.wbg.__wbindgen_closure_wrapper704 = function(arg0, arg1, arg2) {
-        const ret = makeMutClosure(arg0, arg1, 270, __wbg_adapter_28);
+    imports.wbg.__wbindgen_closure_wrapper1016 = function(arg0, arg1, arg2) {
+        const ret = makeMutClosure(arg0, arg1, 406, __wbg_adapter_28);
         return ret;
     };
-    imports.wbg.__wbindgen_closure_wrapper1875 = function(arg0, arg1, arg2) {
-        const ret = makeMutClosure(arg0, arg1, 580, __wbg_adapter_31);
+    imports.wbg.__wbindgen_closure_wrapper1868 = function(arg0, arg1, arg2) {
+        const ret = makeMutClosure(arg0, arg1, 576, __wbg_adapter_31);
         return ret;
     };
-    imports.wbg.__wbindgen_closure_wrapper2137 = function(arg0, arg1, arg2) {
-        const ret = makeMutClosure(arg0, arg1, 653, __wbg_adapter_34);
+    imports.wbg.__wbindgen_closure_wrapper2133 = function(arg0, arg1, arg2) {
+        const ret = makeMutClosure(arg0, arg1, 648, __wbg_adapter_34);
         return ret;
     };
     imports.wbg.__wbindgen_init_externref_table = function() {
diff --git a/pkg/aris_web_app_bg.wasm b/pkg/aris_web_app_bg.wasm
index 8fe12986..eb077f88 100644
Binary files a/pkg/aris_web_app_bg.wasm and b/pkg/aris_web_app_bg.wasm differ
diff --git a/pkg/aris_web_app_bg.wasm.d.ts b/pkg/aris_web_app_bg.wasm.d.ts
index 6f5cc4cf..bca46ec2 100644
--- a/pkg/aris_web_app_bg.wasm.d.ts
+++ b/pkg/aris_web_app_bg.wasm.d.ts
@@ -6,11 +6,11 @@ export function __wbindgen_malloc(a: number, b: number): number;
 export function __wbindgen_realloc(a: number, b: number, c: number, d: number): number;
 export const __wbindgen_export_2: WebAssembly.Table;
 export const __wbindgen_export_3: WebAssembly.Table;
-export function closure269_externref_shim(a: number, b: number, c: number): void;
-export function _dyn_core__ops__function__FnMut_____Output___R_as_wasm_bindgen__closure__WasmClosure___describe__invoke__ha8a700ca1b2368f1(a: number, b: number): void;
-export function closure276_externref_shim(a: number, b: number, c: number): void;
-export function closure579_externref_shim(a: number, b: number, c: number): void;
-export function closure652_externref_shim(a: number, b: number, c: number): void;
+export function closure405_externref_shim(a: number, b: number, c: number): void;
+export function _dyn_core__ops__function__FnMut_____Output___R_as_wasm_bindgen__closure__WasmClosure___describe__invoke__had26f60e34ffd4b2(a: number, b: number): void;
+export function closure412_externref_shim(a: number, b: number, c: number): void;
+export function closure575_externref_shim(a: number, b: number, c: number): void;
+export function closure647_externref_shim(a: number, b: number, c: number): void;
 export function __wbindgen_free(a: number, b: number, c: number): void;
 export function __wbindgen_exn_store(a: number): void;
 export function __externref_table_alloc(): number;
diff --git a/proofImages_dark/Biconditional Complement.png b/proofImages_dark/Biconditional Complement.png
new file mode 100644
index 00000000..d7f011a7
Binary files /dev/null and b/proofImages_dark/Biconditional Complement.png differ
diff --git a/proofImages_dark/Biconditional Contraposition.png b/proofImages_dark/Biconditional Contraposition.png
new file mode 100644
index 00000000..12b87d92
Binary files /dev/null and b/proofImages_dark/Biconditional Contraposition.png differ
diff --git a/proofImages_dark/Biconditional Identity.png b/proofImages_dark/Biconditional Identity.png
new file mode 100644
index 00000000..1c60dd85
Binary files /dev/null and b/proofImages_dark/Biconditional Identity.png differ
diff --git a/proofImages_dark/Biconditional Reduction.png b/proofImages_dark/Biconditional Reduction.png
new file mode 100644
index 00000000..5b547d85
Binary files /dev/null and b/proofImages_dark/Biconditional Reduction.png differ
diff --git a/proofImages_dark/Conditional Absorption.png b/proofImages_dark/Conditional Absorption.png
new file mode 100644
index 00000000..370f0567
Binary files /dev/null and b/proofImages_dark/Conditional Absorption.png differ
diff --git a/proofImages_dark/Biconditional Equivalence.png b/proofImages_dark/Equivalence.png
similarity index 100%
rename from proofImages_dark/Biconditional Equivalence.png
rename to proofImages_dark/Equivalence.png
diff --git a/proofImages_dark/Half DeMorgan.png b/proofImages_dark/Half DeMorgan.png
new file mode 100644
index 00000000..7e837be4
Binary files /dev/null and b/proofImages_dark/Half DeMorgan.png differ
diff --git a/proofImages_dark/Knights and Knaves.png b/proofImages_dark/Knights & Knaves.png
similarity index 100%
rename from proofImages_dark/Knights and Knaves.png
rename to proofImages_dark/Knights & Knaves.png
diff --git a/proofImages_dark/Truth-Functional Consequence.png b/proofImages_dark/Truth-Functional Consequence.png
index 1327ae7b..6365a721 100644
Binary files a/proofImages_dark/Truth-Functional Consequence.png and b/proofImages_dark/Truth-Functional Consequence.png differ
diff --git a/proofImages_light/Biconditional Complement.png b/proofImages_light/Biconditional Complement.png
new file mode 100644
index 00000000..6d7f308c
Binary files /dev/null and b/proofImages_light/Biconditional Complement.png differ
diff --git a/proofImages_light/Biconditional Contraposition.png b/proofImages_light/Biconditional Contraposition.png
new file mode 100644
index 00000000..4e2e9aec
Binary files /dev/null and b/proofImages_light/Biconditional Contraposition.png differ
diff --git a/proofImages_light/Biconditional Identity.png b/proofImages_light/Biconditional Identity.png
new file mode 100644
index 00000000..64918f13
Binary files /dev/null and b/proofImages_light/Biconditional Identity.png differ
diff --git a/proofImages_light/Biconditional Reduction.png b/proofImages_light/Biconditional Reduction.png
new file mode 100644
index 00000000..479415d0
Binary files /dev/null and b/proofImages_light/Biconditional Reduction.png differ
diff --git a/proofImages_light/Conditional Absorption.png b/proofImages_light/Conditional Absorption.png
new file mode 100644
index 00000000..414d8d69
Binary files /dev/null and b/proofImages_light/Conditional Absorption.png differ
diff --git a/proofImages_light/Conditional Complement.png b/proofImages_light/Conditional Complement.png
index 963d5cb7..c766241a 100644
Binary files a/proofImages_light/Conditional Complement.png and b/proofImages_light/Conditional Complement.png differ
diff --git a/proofImages_light/Conditional Identity.png b/proofImages_light/Conditional Identity.png
index 1f730aba..e4356bc7 100644
Binary files a/proofImages_light/Conditional Identity.png and b/proofImages_light/Conditional Identity.png differ
diff --git a/proofImages_light/Conditional Reduction.png b/proofImages_light/Conditional Reduction.png
index 83a494df..9474b72e 100644
Binary files a/proofImages_light/Conditional Reduction.png and b/proofImages_light/Conditional Reduction.png differ
diff --git a/proofImages_light/Biconditional Equivalence.png b/proofImages_light/Equivalence.png
similarity index 100%
rename from proofImages_light/Biconditional Equivalence.png
rename to proofImages_light/Equivalence.png
diff --git a/proofImages_light/Half DeMorgan.png b/proofImages_light/Half DeMorgan.png
new file mode 100644
index 00000000..d666a8d2
Binary files /dev/null and b/proofImages_light/Half DeMorgan.png differ
diff --git a/proofImages_light/Knights and Knaves.png b/proofImages_light/Knights & Knaves.png
similarity index 100%
rename from proofImages_light/Knights and Knaves.png
rename to proofImages_light/Knights & Knaves.png
diff --git a/proofImages_light/Truth-Functional Consequence.png b/proofImages_light/Truth-Functional Consequence.png
index 01f4e387..8cd364d9 100644
Binary files a/proofImages_light/Truth-Functional Consequence.png and b/proofImages_light/Truth-Functional Consequence.png differ
