diff --git a/README.md b/README.md
index 895d77f..b44eef1 100644
--- a/README.md
+++ b/README.md
@@ -8,7 +8,7 @@ It is influenced by the commercial Hyperslate Proof Assistant which has many mor
 
 ## Sample Proofs
 Some basic tautologies:
-[A -> A, (A /\ B) => (B /\ A), (A /\ (A -> B)) -> B](https://james-oswald.github.io/lazyslate/?proof=N4Igdg9gJgpgziAXAbVASykgDAGnAQwFsYkQsQ8YAPABwCd440IxSBBCkAKwFc4AXNADM0AY3yCWpfHDg9inGhCaTWiUFSQAWAOwBWPAE8kAJjMBfcznSZEARjxgiJRCACSQgARtP%2DABb4YN6c1PSMzGogABTC3t4AlJy8AsJiEhGkwm6KymiqSBraWiZGSADMAJwAbJbWIBimjs6kJiG0DLIZrlGBUHEAQol4yYIi4vmuMnIKeEoqXYWIABxluCDGiCZ2JrU25U0KrmVtYZ1S3b2e%2DQlJfKNpEyC92bO5E4tLWg7rSHp2S7t6rYtAcXCAtCcOkxziAOMM7qlxl0nmAoABRHLzc6LHRVEE%2DRBlKo7Kx7RAGAiHEB6SHhGH9W4pMbpGG9DGvLFqRYVExLUqEvRaQENRBVUGkADCEEIhB4%2DHSADcYJ4pWBeGBRKoEJR2nTIjEvD1UQN4p4jX1rmx4kNuAjmY8spi8gsQJpEDpdPyqjoKsLbDpxa4dLSzvrLj4DSabSNESzIlN5CQOc7sa6kHYyiY1hss1g%2DUg+ZSwUsQ9DInDbUyHsi2U73mn7CYqmV+WU9L7SUCkBVAyAKqXkZGfINGfckazUeyQHMU1yG3YtFoWwS22V8%2DY1k4qXZyDrTmXSAz4VXx5FhFOZ%2DW3RmdCUCXoykLOyK7N8t2CALLQeCeAAKLBgMBtRAUIoUHWJzTiIcrmtGDR1jB0hBeac3hda8TAqQsNiqJYanMABdPAABs0DAABrBAUGQXA7EI5ASi0OiSj0OiQTKOiDHYnBkBbKo6IDJZ+JwCo6L5Hc6J7cTuJ3HBX3w%2DDzCAA)
+[A -> A, (A /\ B) => (B /\ A), (A /\ (A -> B)) -> B](https://rairlab.github.io/lazyslate/?proof=N4Igdg9gJgpgziAXAbVASykgDAGnAQwFsYkQsQ8YAPABwCd440IxSBBCkAKwFc4AXNADM0AY3yCWpfHDg9inGhCaTWiUFSQAWAOwBWPAE8kAJjMBfcznSZEARjxgiJRCACSQgARtP%2DABb4YN6c1PSMzGogABTC3t4AlJy8AsJiEhGkwm6KymiqSBraWiZGSADMAJwAbJbWIBimjs6kJiG0DLIZrlGBUHEAQol4yYIi4vmuMnIKeEoqXYWIABxluCDGiCZ2JrU25U0KrmVtYZ1S3b2e%2DQlJfKNpEyC92bO5E4tLWg7rSHp2S7t6rYtAcXCAtCcOkxziAOMM7qlxl0nmAoABRHLzc6LHRVEE%2DRBlKo7Kx7RAGAiHEB6SHhGH9W4pMbpGG9DGvLFqRYVExLUqEvRaQENRBVUGkADCEEIhB4%2DHSADcYJ4pWBeGBRKoEJR2nTIjEvD1UQN4p4jX1rmx4kNuAjmY8spi8gsQJpEDpdPyqjoKsLbDpxa4dLSzvrLj4DSabSNESzIlN5CQOc7sa6kHYyiY1hss1g%2DUg+ZSwUsQ9DInDbUyHsi2U73mn7CYqmV+WU9L7SUCkBVAyAKqXkZGfINGfckazUeyQHMU1yG3YtFoWwS22V8%2DY1k4qXZyDrTmXSAz4VXx5FhFOZ%2DW3RmdCUCXoykLOyK7N8t2CALLQeCeAAKLBgMBtRAUIoUHWJzTiIcrmtGDR1jB0hBeac3hda8TAqQsNiqJYanMABdPAABs0DAABrBAUGQXA7EI5ASi0OiSj0OiQTKOiDHYnBkBbKo6IDJZ+JwCo6L5Hc6J7cTuJ3HBX3w%2DDzCAA)
 
 ## Building
 
@@ -35,7 +35,7 @@ introduction and elimination.
 We enumerate all of our inference rules here.
 For an example of all of a proof space with
 proofs containing examples of all the infrence rules
-see [This Proof](https://james-oswald.github.io/lazyslate?proof=N4Igdg9gJgpgziAXAbVASykgDAGnAQwFsZs8YAPABwCd440IwkQBBEPAKwFc4AXNAGZoAxvn6Nm+OHC7F2IShHrimiUOSQBGACwB2bXgCeWgGzaAvuZzpMiTXjBESiEJvkUadBqpAAKCNQABCyBAEIAlPLcfIIiYt7MAQCS8orKCWogGnbaJrggxogAzEUATJbWIBhIpQ5ONWRUtNIZfpC8wZGcPPxCoirM7Sl4aWgDmdmlRQYFSNoAHCYVNkhFdXIuRe5NXhIuAIpRPbH9rYIAoqlKYxnqNWVGq6W6y1W2M44bINrbni17bQgHX2XRA0V6cXGICkMjkI2u4zuiAAnPZZsVSlhXtVEABWdbOEC437NegA3yCYKBEFHGJ9eIAmGyEjw9J7JGlTGPHJFbG2EwEpACkAeUmtNjdOmQ1pMuEKBG3LJaLBowo6cpWFaIXSCly6Em7HwSsHHelQ9qXVk3dlKvGo7m4zl8pDzXUgeYG-4+XztTq0iGnRnSZlXNmqJG5WrozS4+bOlG65GNP5knyHSUBhk+C6h63h2245Gu9HTXHxzT5T7OCvJsXk300jMnLOSYNy0aI216VWrbQWTVvLRoqvMTRuWuG5gUgSBH1AzrU0Hg5tQ2Us+VhpBIwv5NWx8tRkcuTSlT2pqf4MBQKkRf0rmVX4YbvNb23IrAzQplJYDnGaNYEBs-4Tl6zDGsuZoym264doq2TzLiOrRiYmjlh89Q5CB54uKEd6QUGsIwQqNrZEWwp7si5b4oBhIxmerS+Je14hLeTb4T4a65p22RjvMxZqiYZa-rYmjCkeolYeKeHSoyV6Ws+3FDkU5FPHGwlaEhR6uPqkkArhbEyRxclcXBWilCYKkYi86l2MW4nFqKk4uP4QQsUupqGa2hEmSRGlYEmJbaFiNmaAFWmhfRAIAMLSYG2YCPJsG+bZJhRl+RRqZUOJcjRzCYpFPgxQZcXMDmVqKYgmLPNy0zBVltilMOGEgI1BVTpSIRRe5UolS4nHlaZKWWTGmVapybqcm1zmUqEgRdbFLZ9dBPn5pMWAlNyMb9vV9y6lMuk+PpJo9Yt0LLQNyWNboaVaLiQk7ZV6EbKUMyOaBLjgR5vVnd5F2rRp43RoW8alNRR6gwdzBFcdmZQgEiXEf9tkLA6ykg2JzXmVNrALau50KYNL1FEhAm8jZ1W5S4zzYy5N7dbDrTJCtr6TNopQBelP4PaUdmYx6kPTTOIS0259P3gCghPklSMvVgu5ILiRR1WNYUYezAs48Vp39QTl2CfxfnxkrbpK9jR0QZ5LhlbrMu6MBJZOjZRRNV8zs0x1YRi+xXkhn9LM1Lo8yfqYlFO4eGEPCKOzvX4ghC57uNnAIAhS4j-vFKJHNzLoyuDsUAFHhtUcplJWt479Nvp+zyLDTnRtPc40wa+bX3a-j0vpyUiGbRZRtgxH1Fvdhsfx6xMPixx7dpxMqwVsHdh20bGMbMpzeJxLCXMzPxTrZZZRkw9xMmzpxd1t6M1+mXUEVx32-71ndgmKNecZbqr+n05mvj97Vub37d-swAl+UGRtVau2RO7ZOdN16TxvtPJEylFibWBjZIKuo0Efxjp9E65dfaVzvriFCPdc44m0C7QkZCzYwJ9u2eBtoMrGyBs-Uh4cvhs2xtghmG8-74IQboCyNVGrxm0AXDCIi15X24QjTcd8ULzzKBqAAungAANmgMAABrBAKBkC4E0Mo5A+IigGIFMYnAyA1ilAMQYKx5iay6AMUmBxdj7DIgMa6Nxdi1gngMToHAPi7H4lEr4oJzjkCNX8Z48JtRMQGJepEuJlisC+NdKDXxSY0nmK5Jk8JApnhxJ1DzOJSYlYGOdjgUp5iNrKTKUYkwZSdQZTKQYJpVTTG2Isa6MoZSkxs2sfYPp5i0EiJ6TgEZijzBAA)
+see [This Proof](https://rairlab.github.io/lazyslate?proof=N4Igdg9gJgpgziAXAbVASykgDAGnAQwFsZs8YAPABwCd440IwkQBBEPAKwFc4AXNAGZoAxvn6Nm+OHC7F2IShHrimiUOSQBGACwB2bXgCeWgGzaAvuZzpMiTXjBESiEJvkUadBqpAAKCNQABCyBAEIAlPLcfIIiYt7MAQCS8orKCWogGnbaJrggxogAzEUATJbWIBhIpQ5ONWRUtNIZfpC8wZGcPPxCoirM7Sl4aWgDmdmlRQYFSNoAHCYVNkhFdXIuRe5NXhIuAIpRPbH9rYIAoqlKYxnqNWVGq6W6y1W2M44bINrbni17bQgHX2XRA0V6cXGICkMjkI2u4zuiAAnPZZsVSlhXtVEABWdbOEC437NegA3yCYKBEFHGJ9eIAmGyEjw9J7JGlTGPHJFbG2EwEpACkAeUmtNjdOmQ1pMuEKBG3LJaLBowo6cpWFaIXSCly6Em7HwSsHHelQ9qXVk3dlKvGo7m4zl8pDzXUgeYG-4+XztTq0iGnRnSZlXNmqJG5WrozS4+bOlG65GNP5knyHSUBhk+C6h63h2245Gu9HTXHxzT5T7OCvJsXk300jMnLOSYNy0aI216VWrbQWTVvLRoqvMTRuWuG5gUgSBH1AzrU0Hg5tQ2Us+VhpBIwv5NWx8tRkcuTSlT2pqf4MBQKkRf0rmVX4YbvNb23IrAzQplJYDnGaNYEBs-4Tl6zDGsuZoym264doq2TzLiOrRiYmjlh89Q5CB54uKEd6QUGsIwQqNrZEWwp7si5b4oBhIxmerS+Je14hLeTb4T4a65p22RjvMxZqiYZa-rYmjCkeolYeKeHSoyV6Ws+3FDkU5FPHGwlaEhR6uPqkkArhbEyRxclcXBWilCYKkYi86l2MW4nFqKk4uP4QQsUupqGa2hEmSRGlYEmJbaFiNmaAFWmhfRAIAMLSYG2YCPJsG+bZJhRl+RRqZUOJcjRzCYpFPgxQZcXMDmVqKYgmLPNy0zBVltilMOGEgI1BVTpSIRRe5UolS4nHlaZKWWTGmVapybqcm1zmUqEgRdbFLZ9dBPn5pMWAlNyMb9vV9y6lMuk+PpJo9Yt0LLQNyWNboaVaLiQk7ZV6EbKUMyOaBLjgR5vVnd5F2rRp43RoW8alNRR6gwdzBFcdmZQgEiXEf9tkLA6ykg2JzXmVNrALau50KYNL1FEhAm8jZ1W5S4zzYy5N7dbDrTJCtr6TNopQBelP4PaUdmYx6kPTTOIS0259P3gCghPklSMvVgu5ILiRR1WNYUYezAs48Vp39QTl2CfxfnxkrbpK9jR0QZ5LhlbrMu6MBJZOjZRRNV8zs0x1YRi+xXkhn9LM1Lo8yfqYlFO4eGEPCKOzvX4ghC57uNnAIAhS4j-vFKJHNzLoyuDsUAFHhtUcplJWt479Nvp+zyLDTnRtPc40wa+bX3a-j0vpyUiGbRZRtgxH1Fvdhsfx6xMPixx7dpxMqwVsHdh20bGMbMpzeJxLCXMzPxTrZZZRkw9xMmzpxd1t6M1+mXUEVx32-71ndgmKNecZbqr+n05mvj97Vub37d-swAl+UGRtVau2RO7ZOdN16TxvtPJEylFibWBjZIKuo0Efxjp9E65dfaVzvriFCPdc44m0C7QkZCzYwJ9u2eBtoMrGyBs-Uh4cvhs2xtghmG8-74IQboCyNVGrxm0AXDCIi15X24QjTcd8ULzzKBqAAungAANmgMAABrBAKBkC4E0Mo5A+IigGIFMYnAyA1ilAMQYKx5iay6AMUmBxdj7DIgMa6Nxdi1gngMToHAPi7H4lEr4oJzjkCNX8Z48JtRMQGJepEuJlisC+NdKDXxSY0nmK5Jk8JApnhxJ1DzOJSYlYGOdjgUp5iNrKTKUYkwZSdQZTKQYJpVTTG2Isa6MoZSkxs2sfYPp5i0EiJ6TgEZijzBAA)
 
 ```
 Negation Introduction (Reductio ad absurdum):