diff --git a/aris/src/expr.rs b/aris/src/expr.rs
index 4a05920d..2a971738 100644
--- a/aris/src/expr.rs
+++ b/aris/src/expr.rs
@@ -8,7 +8,7 @@ Parsing an expression that's statically known to be valid:
 ```
 use aris::parser::parse_unwrap as p;
 
-let expr1 = p("forall x, p(x) -> (Q & R)");
+let expr1 = p("forall x p(x) -> (Q & R)");
 ```
 
 Parsing a potentially malformed expression (e.g. user input):
@@ -389,7 +389,7 @@ pub fn unify(mut c: HashSet<Constraint>) -> Option<Substitution> {
         }
         (Expr::Apply { func: sf, args: sa }, Expr::Apply { func: tf, args: ta }) if sa.len() == ta.len() => {
             c.insert(Constraint::Equal(*sf, *tf));
-            c.extend(sa.into_iter().zip(ta.into_iter()).map(|(x, y)| Constraint::Equal(x, y)));
+            c.extend(sa.into_iter().zip(ta).map(|(x, y)| Constraint::Equal(x, y)));
             unify(c)
         }
         (Expr::Assoc { op: so, exprs: se }, Expr::Assoc { op: to, exprs: te }) if so == to && se.len() == te.len() => {
@@ -887,7 +887,7 @@ impl Expr {
                     Expr::Var { name: format!("{i}") }
                 }
                 // push the name onto gamma from the actual quantifier,
-                // Example: for forall x, P(x)
+                // Example: for forall x P(x)
                 // push x onto gamma
                 // save the length of gamma before recursing, to use as the new name
                 Expr::Quant { kind, name, body } => {
@@ -966,14 +966,14 @@ impl Expr {
         })
     }
 
-    /// 7a1. forall x, (phi(x) ∧ psi) == (forall x, phi(x)) ∧ psi
-    /// 7a2. exists x, (phi(x) ∧ psi) == (exists x, phi(x)) ∧ psi
-    /// 7b1. forall x, (phi(x) ∨ psi) == (forall x, phi(x)) ∨ psi
-    /// 7b2. exists x, (phi(x) ∨ psi) == (exists x, phi(x)) ∨ psi
-    /// 7c1. forall x, (phi(x) → psi) == (exists x, phi(x)) → psi (! Expr::Quantifier changes!)
-    /// 7c2. exists x, (phi(x) → psi) == (forall x, phi(x)) → psi (! Expr::Quantifier changes!)
-    /// 7d1. forall x, (psi → phi(x)) == psi → (forall x, phi(x))
-    /// 7d2. exists x, (psi → phi(x)) == psi → (exists x, phi(x))
+    /// 7a1. forall x (phi(x) ∧ psi) == (forall x phi(x)) ∧ psi
+    /// 7a2. exists x (phi(x) ∧ psi) == (exists x phi(x)) ∧ psi
+    /// 7b1. forall x (phi(x) ∨ psi) == (forall x phi(x)) ∨ psi
+    /// 7b2. exists x (phi(x) ∨ psi) == (exists x phi(x)) ∨ psi
+    /// 7c1. forall x (phi(x) → psi) == (exists x phi(x)) → psi (! Expr::Quantifier changes!)
+    /// 7c2. exists x (phi(x) → psi) == (forall x phi(x)) → psi (! Expr::Quantifier changes!)
+    /// 7d1. forall x (psi → phi(x)) == psi → (forall x phi(x))
+    /// 7d2. exists x (psi → phi(x)) == psi → (exists x phi(x))
     pub fn normalize_prenex_laws(self) -> Expr {
         let transform_7ab = |op: Op, exprs: Vec<Expr>| {
             // hoist a forall out of an and/or when the binder won't capture any of the other arms
@@ -1534,11 +1534,11 @@ mod tests {
     #[test]
     fn test_subst() {
         use crate::parser::parse_unwrap as p;
-        assert_eq!(subst(p("x & forall x, x"), "x", p("y")), p("y & forall x, x")); // hit (true, _) case in Expr::Quantifier
-        assert_eq!(subst(p("forall x, x & y"), "y", p("x")), p("forall x0, x0 & x")); // hit (false, true) case in Expr::Quantifier
-        assert_eq!(subst(p("forall x, x & y"), "y", p("z")), p("forall x, x & z")); // hit (false, false) case in Expr::Quantifier
-        assert_eq!(subst(p("forall f, f(x) & g(y, z)"), "g", p("h")), p("forall f, f(x) & h(y, z)"));
-        assert_eq!(subst(p("forall f, f(x) & g(y, z)"), "g", p("f")), p("forall f0, f0(x) & f(y, z)"));
+        assert_eq!(subst(p("x & forall x x"), "x", p("y")), p("y & forall x x")); // hit (true, _) case in Expr::Quantifier
+        assert_eq!(subst(p("forall x x & y"), "y", p("x")), p("forall x0 x0 & x")); // hit (false, true) case in Expr::Quantifier
+        assert_eq!(subst(p("forall x x & y"), "y", p("z")), p("forall x x & z")); // hit (false, false) case in Expr::Quantifier
+        assert_eq!(subst(p("forall f f(x) & g(y, z)"), "g", p("h")), p("forall f f(x) & h(y, z)"));
+        assert_eq!(subst(p("forall f f(x) & g(y, z)"), "g", p("f")), p("forall f0 f0(x) & f(y, z)"));
     }
 
     #[test]
@@ -1556,15 +1556,15 @@ mod tests {
             }
             ret
         };
-        println!("{:?}", u("x", "forall y, y"));
-        println!("{:?}", u("forall y, y", "y"));
+        println!("{:?}", u("x", "forall y y"));
+        println!("{:?}", u("forall y y", "y"));
         println!("{:?}", u("x", "x"));
-        assert_eq!(u("forall x, x", "forall y, y"), Some(Substitution(vec![]))); // should be equal with no substitution since unification is modulo alpha equivalence
+        assert_eq!(u("forall x x", "forall y y"), Some(Substitution(vec![]))); // should be equal with no substitution since unification is modulo alpha equivalence
         println!("{:?}", u("f(x,y,z)", "g(x,y,y)"));
         println!("{:?}", u("g(x,y,y)", "f(x,y,z)"));
-        println!("{:?}", u("forall foo, foo(x,y,z) & bar", "forall bar, bar(x,y,z) & baz"));
+        println!("{:?}", u("forall foo foo(x,y,z) & bar", "forall bar bar(x,y,z) & baz"));
 
-        assert_eq!(u("forall x, z", "forall y, y"), None);
+        assert_eq!(u("forall x z", "forall y y"), None);
         assert_eq!(u("x & y", "x | y"), None);
     }
 
diff --git a/aris/src/parser.rs b/aris/src/parser.rs
index a46d0202..5941e489 100644
--- a/aris/src/parser.rs
+++ b/aris/src/parser.rs
@@ -87,8 +87,12 @@ fn quantifier(input: &str) -> IResult<&str, QuantKind> {
     alt((forall_quantifier, exists_quantifier))(input)
 }
 
+fn space_after_quantifier(input: &str) -> IResult<&str, ()> {
+    value((), many1(one_of(" \t")))(input)
+}
+
 fn binder(input: &str) -> IResult<&str, Expr> {
-    map(tuple((preceded(space, quantifier), preceded(space, variable), preceded(tuple((space, tag(","), space)), expr))), |(kind, name, body)| Expr::Quant { kind, name, body: Box::new(body) })(input)
+    map(tuple((preceded(space, quantifier), preceded(space, variable), preceded(space_after_quantifier, expr))), |(kind, name, body)| Expr::Quant { kind, name, body: Box::new(body) })(input)
 }
 
 fn impl_term(input: &str) -> IResult<&str, Expr> {
@@ -165,11 +169,11 @@ fn test_parser() {
     println!("{:?}", predicate("a(   b, c)"));
     println!("{:?}", predicate("s(s(s(s(s(z)))))"));
     println!("{:?}", expr("a & b & c(x,y)\n"));
-    println!("{:?}", expr("forall a, (b & c)\n"));
-    let e = expr("exists x, (Tet(x) & SameCol(x, b)) -> ~forall x, (Tet(x) -> LeftOf(x, b))\n").unwrap();
+    println!("{:?}", expr("forall a (b & c)\n"));
+    let e = expr("exists x (Tet(x) & SameCol(x, b)) -> ~forall x (Tet(x) -> LeftOf(x, b))\n").unwrap();
     let fv = free_vars(&e.1);
     println!("{e:?} {fv:?}");
-    let e = expr("forall a, forall b, ((forall x, in(x,a) <-> in(x,b)) -> eq(a,b))\n").unwrap();
+    let e = expr("forall a forall b ((forall x in(x,a) <-> in(x,b)) -> eq(a,b))\n").unwrap();
     let fv = free_vars(&e.1);
     assert_eq!(fv, ["eq", "in"].iter().map(|x| String::from(*x)).collect());
     println!("{e:?} {fv:?}");
diff --git a/aris/src/proofs.rs b/aris/src/proofs.rs
index 559ed52e..fbcecbf4 100644
--- a/aris/src/proofs.rs
+++ b/aris/src/proofs.rs
@@ -255,7 +255,7 @@ pub trait Proof: Sized {
     }
     fn contained_justifications(&self, include_premises: bool) -> HashSet<PjRef<Self>> {
         let mut ret = self.lines().into_iter().filter_map(|x| x.fold(hlist![|r: Self::JustificationReference| Some(vec![r].into_iter().map(Coproduct::inject).collect()), |r: Self::SubproofReference| self.lookup_subproof(&r).map(|sub| sub.contained_justifications(include_premises)),])).fold(HashSet::new(), |mut x, y| {
-            x.extend(y.into_iter());
+            x.extend(y);
             x
         });
         if include_premises {
diff --git a/aris/src/proofs/proof_tests.rs b/aris/src/proofs/proof_tests.rs
index f85a49e4..e56842a9 100644
--- a/aris/src/proofs/proof_tests.rs
+++ b/aris/src/proofs/proof_tests.rs
@@ -145,7 +145,7 @@ pub fn test_contelim<P: Proof>() -> (P, Vec<PjRef<P>>, Vec<PjRef<P>>) {
     let mut prf = P::new();
     let r1 = prf.add_premise(p("_|_"));
     let r2 = prf.add_premise(p("A & B"));
-    let r3 = prf.add_step(Justification(p("forall x, x & ~ x"), RuleM::ContradictionElim, vec![i(r1)], vec![]));
+    let r3 = prf.add_step(Justification(p("forall x x & ~ x"), RuleM::ContradictionElim, vec![i(r1)], vec![]));
     let r4 = prf.add_step(Justification(p("Q"), RuleM::ContradictionElim, vec![i(r2)], vec![]));
     (prf, vec![i(r3)], vec![i(r4)])
 }
@@ -459,7 +459,7 @@ where
     use self::coproduct_inject as i;
     use crate::parser::parse_unwrap as p;
     let mut prf = P::new();
-    let r1 = prf.add_premise(p("forall x, p(x)"));
+    let r1 = prf.add_premise(p("forall x p(x)"));
     let r2 = prf.add_step(Justification(p("p(a)"), RuleM::ForallElim, vec![i(r1.clone())], vec![]));
     let r3 = prf.add_step(Justification(p("q(x)"), RuleM::ForallElim, vec![i(r1.clone())], vec![]));
     let r4 = prf.add_step(Justification(p("p(A & B & C & D)"), RuleM::ForallElim, vec![i(r1)], vec![]));
@@ -475,8 +475,8 @@ where
     use self::coproduct_inject as i;
     use crate::parser::parse_unwrap as p;
     let mut prf = P::new();
-    let r1 = prf.add_premise(p("forall x, p(x)"));
-    let r2 = prf.add_premise(p("forall x, q(x)"));
+    let r1 = prf.add_premise(p("forall x p(x)"));
+    let r2 = prf.add_premise(p("forall x q(x)"));
     let r3 = prf.add_premise(p("r(c)"));
     let r4 = prf.add_subproof();
     let (r5, r6, r7) = prf
@@ -487,8 +487,8 @@ where
             (r5, r6, r7)
         })
         .unwrap();
-    let r8 = prf.add_step(Justification(p("forall y, p(y) & q(y)"), RuleM::ForallIntro, vec![], vec![r4.clone()]));
-    let r9 = prf.add_step(Justification(p("forall y, p(a) & q(y)"), RuleM::ForallIntro, vec![], vec![r4.clone()]));
+    let r8 = prf.add_step(Justification(p("forall y p(y) & q(y)"), RuleM::ForallIntro, vec![], vec![r4.clone()]));
+    let r9 = prf.add_step(Justification(p("forall y p(a) & q(y)"), RuleM::ForallIntro, vec![], vec![r4.clone()]));
     let r10 = prf.add_subproof();
     let r11 = prf
         .with_mut_subproof(&r10, |sub| {
@@ -499,7 +499,7 @@ where
             r11
         })
         .unwrap();
-    let r12 = prf.add_step(Justification(p("forall y, r(y)"), RuleM::ForallIntro, vec![], vec![r10.clone()]));
+    let r12 = prf.add_step(Justification(p("forall y r(y)"), RuleM::ForallIntro, vec![], vec![r10.clone()]));
     let r13 = prf.add_subproof();
     let (r17, r18, r19) = prf
         .with_mut_subproof(&r13, |sub1| {
@@ -508,11 +508,11 @@ where
                 .with_mut_subproof(&r14, |sub2| {
                     let r15 = sub2.add_subproof();
                     let r17 = sub2.with_mut_subproof(&r15, |sub3| sub3.add_step(Justification(p("s(a, b)"), RuleM::Reit, vec![], vec![]))).unwrap();
-                    let r18 = sub2.add_step(Justification(p("forall y, s(a, y)"), RuleM::ForallIntro, vec![], vec![r15]));
+                    let r18 = sub2.add_step(Justification(p("forall y s(a, y)"), RuleM::ForallIntro, vec![], vec![r15]));
                     (r17, r18)
                 })
                 .unwrap();
-            let r19 = sub1.add_step(Justification(p("forall x, forall y, s(x, y)"), RuleM::ForallIntro, vec![], vec![r14]));
+            let r19 = sub1.add_step(Justification(p("forall x forall y s(x, y)"), RuleM::ForallIntro, vec![], vec![r14]));
             (r17, r18, r19)
         })
         .unwrap();
@@ -525,7 +525,7 @@ where
             sub.add_step(Justification(p("a"), RuleM::Reit, vec![i(r21)], vec![]))
         })
         .unwrap();
-    let r23 = prf.add_step(Justification(p("forall x, x"), RuleM::ForallIntro, vec![], vec![r20]));
+    let r23 = prf.add_step(Justification(p("forall x x"), RuleM::ForallIntro, vec![], vec![r20]));
     (prf, vec![i(r5), i(r6), i(r7), i(r8), i(r11), i(r18), i(r19), i(r22)], vec![i(r9), i(r12), i(r17), i(r23)])
 }
 
@@ -541,16 +541,16 @@ where
 
     let r1 = prf.add_premise(p("p(a)"));
     let r2 = prf.add_step(Justification(p("p(b) & p(b)"), RuleM::Reit, vec![], vec![]));
-    let r3 = prf.add_step(Justification(p("exists x, p(x)"), RuleM::ExistsIntro, vec![i(r1.clone())], vec![]));
-    let r4 = prf.add_step(Justification(p("exists x, p(a)"), RuleM::ExistsIntro, vec![i(r1.clone())], vec![]));
-    let r5 = prf.add_step(Justification(p("exists x, p(b)"), RuleM::ExistsIntro, vec![i(r1)], vec![]));
-    let r6 = prf.add_step(Justification(p("exists x, p(x) & p(x)"), RuleM::ExistsIntro, vec![i(r2.clone())], vec![]));
-    let r7 = prf.add_step(Justification(p("exists x, p(b) & p(x)"), RuleM::ExistsIntro, vec![i(r2.clone())], vec![]));
-    let r8 = prf.add_step(Justification(p("exists x, p(x) & p(b)"), RuleM::ExistsIntro, vec![i(r2.clone())], vec![]));
-    let r9 = prf.add_step(Justification(p("exists x, p(b) & p(b)"), RuleM::ExistsIntro, vec![i(r2.clone())], vec![]));
-    let r10 = prf.add_step(Justification(p("exists x, p(y) & p(b)"), RuleM::ExistsIntro, vec![i(r2.clone())], vec![]));
-    let r11 = prf.add_step(Justification(p("exists x, p(a) & p(b)"), RuleM::ExistsIntro, vec![i(r2.clone())], vec![]));
-    let r12 = prf.add_step(Justification(p("exists x, p(y) & p(x)"), RuleM::ExistsIntro, vec![i(r2)], vec![]));
+    let r3 = prf.add_step(Justification(p("exists x p(x)"), RuleM::ExistsIntro, vec![i(r1.clone())], vec![]));
+    let r4 = prf.add_step(Justification(p("exists x p(a)"), RuleM::ExistsIntro, vec![i(r1.clone())], vec![]));
+    let r5 = prf.add_step(Justification(p("exists x p(b)"), RuleM::ExistsIntro, vec![i(r1)], vec![]));
+    let r6 = prf.add_step(Justification(p("exists x p(x) & p(x)"), RuleM::ExistsIntro, vec![i(r2.clone())], vec![]));
+    let r7 = prf.add_step(Justification(p("exists x p(b) & p(x)"), RuleM::ExistsIntro, vec![i(r2.clone())], vec![]));
+    let r8 = prf.add_step(Justification(p("exists x p(x) & p(b)"), RuleM::ExistsIntro, vec![i(r2.clone())], vec![]));
+    let r9 = prf.add_step(Justification(p("exists x p(b) & p(b)"), RuleM::ExistsIntro, vec![i(r2.clone())], vec![]));
+    let r10 = prf.add_step(Justification(p("exists x p(y) & p(b)"), RuleM::ExistsIntro, vec![i(r2.clone())], vec![]));
+    let r11 = prf.add_step(Justification(p("exists x p(a) & p(b)"), RuleM::ExistsIntro, vec![i(r2.clone())], vec![]));
+    let r12 = prf.add_step(Justification(p("exists x p(y) & p(x)"), RuleM::ExistsIntro, vec![i(r2)], vec![]));
 
     (prf, vec![i(r3), i(r4), i(r6), i(r7), i(r8), i(r9)], vec![i(r5), i(r10), i(r11), i(r12)])
 }
@@ -563,9 +563,9 @@ where
     use self::coproduct_inject as i;
     use crate::parser::parse_unwrap as p;
     let mut prf = P::new();
-    let r1 = prf.add_premise(p("exists x, p(x)"));
+    let r1 = prf.add_premise(p("exists x p(x)"));
     let r2 = prf.add_premise(p("p(a) -> q(a)"));
-    let r3 = prf.add_premise(p("forall b, (p(b) -> r(b))"));
+    let r3 = prf.add_premise(p("forall b (p(b) -> r(b))"));
     let r4 = prf.add_subproof();
     let (r6, r7, r8, r9, r10) = prf
         .with_mut_subproof(&r4, |sub| {
@@ -573,28 +573,28 @@ where
             let r6 = sub.add_step(Justification(p("q(a)"), RuleM::ImpElim, vec![i(r2.clone()), i(r5.clone())], vec![]));
             let r7 = sub.add_step(Justification(p("p(a) -> r(a)"), RuleM::ForallElim, vec![i(r3.clone())], vec![]));
             let r8 = sub.add_step(Justification(p("r(a)"), RuleM::ImpElim, vec![i(r7.clone()), i(r5)], vec![]));
-            let r9 = sub.add_step(Justification(p("exists x, q(x)"), RuleM::ExistsIntro, vec![i(r6.clone())], vec![]));
-            let r10 = sub.add_step(Justification(p("exists x, r(x)"), RuleM::ExistsIntro, vec![i(r8.clone())], vec![]));
+            let r9 = sub.add_step(Justification(p("exists x q(x)"), RuleM::ExistsIntro, vec![i(r6.clone())], vec![]));
+            let r10 = sub.add_step(Justification(p("exists x r(x)"), RuleM::ExistsIntro, vec![i(r8.clone())], vec![]));
             (r6, r7, r8, r9, r10)
         })
         .unwrap();
-    let r11 = prf.add_step(Justification(p("exists x, q(x)"), RuleM::ExistsElim, vec![i(r1.clone())], vec![r4.clone()]));
-    let r12 = prf.add_step(Justification(p("exists x, r(x)"), RuleM::ExistsElim, vec![i(r1.clone())], vec![r4.clone()]));
+    let r11 = prf.add_step(Justification(p("exists x q(x)"), RuleM::ExistsElim, vec![i(r1.clone())], vec![r4.clone()]));
+    let r12 = prf.add_step(Justification(p("exists x r(x)"), RuleM::ExistsElim, vec![i(r1.clone())], vec![r4.clone()]));
     let r13 = prf.add_step(Justification(p("r(a)"), RuleM::ExistsElim, vec![i(r1.clone())], vec![r4.clone()]));
 
-    let s1 = prf.add_premise(p("forall y, man(y) → mortal(y)"));
-    let s2 = prf.add_premise(p("exists x, man(x)"));
+    let s1 = prf.add_premise(p("forall y man(y) → mortal(y)"));
+    let s2 = prf.add_premise(p("exists x man(x)"));
     let s3 = prf.add_subproof();
     let (s5, s6, s7) = prf
         .with_mut_subproof(&s3, |sub| {
             let s4 = sub.add_premise(p("man(socrates)"));
             let s5 = sub.add_step(Justification(p("man(socrates) → mortal(socrates)"), RuleM::ForallElim, vec![i(s1.clone())], vec![]));
             let s6 = sub.add_step(Justification(p("mortal(socrates)"), RuleM::ImpElim, vec![i(s4), i(s5.clone())], vec![]));
-            let s7 = sub.add_step(Justification(p("exists foo, mortal(foo)"), RuleM::ExistsIntro, vec![i(s6.clone())], vec![]));
+            let s7 = sub.add_step(Justification(p("exists foo mortal(foo)"), RuleM::ExistsIntro, vec![i(s6.clone())], vec![]));
             (s5, s6, s7)
         })
         .unwrap();
-    let s8 = prf.add_step(Justification(p("exists foo, mortal(foo)"), RuleM::ExistsElim, vec![i(s2)], vec![s3.clone()]));
+    let s8 = prf.add_step(Justification(p("exists foo mortal(foo)"), RuleM::ExistsElim, vec![i(s2)], vec![s3.clone()]));
 
     let t1 = prf.add_step(Justification(p("p(a) -> r(a)"), RuleM::ForallElim, vec![i(r3.clone())], vec![]));
     let t2 = prf.add_subproof();
@@ -602,18 +602,18 @@ where
         .with_mut_subproof(&t2, |sub| {
             let t3 = sub.add_premise(p("p(a)"));
             let t4 = sub.add_step(Justification(p("r(a)"), RuleM::ImpElim, vec![i(t1.clone()), i(t3)], vec![]));
-            let t5 = sub.add_step(Justification(p("exists x, r(x)"), RuleM::ExistsIntro, vec![i(t4.clone())], vec![]));
+            let t5 = sub.add_step(Justification(p("exists x r(x)"), RuleM::ExistsIntro, vec![i(t4.clone())], vec![]));
             (t4, t5)
         })
         .unwrap();
-    let t6 = prf.add_step(Justification(p("exists x, r(x)"), RuleM::ExistsElim, vec![i(r1.clone())], vec![t2.clone()]));
+    let t6 = prf.add_step(Justification(p("exists x r(x)"), RuleM::ExistsElim, vec![i(r1.clone())], vec![t2.clone()]));
 
     let u1 = prf.add_subproof();
-    let u2 = prf.add_premise(p("forall c, forall d, p(c) -> s(d)"));
+    let u2 = prf.add_premise(p("forall c forall d p(c) -> s(d)"));
     let (u4, u5, u6) = prf
         .with_mut_subproof(&u1, |sub| {
             let u3 = sub.add_premise(p("p(a)"));
-            let u4 = sub.add_step(Justification(p("forall d, p(a) -> s(d)"), RuleM::ForallElim, vec![i(u2.clone())], vec![]));
+            let u4 = sub.add_step(Justification(p("forall d p(a) -> s(d)"), RuleM::ForallElim, vec![i(u2.clone())], vec![]));
             let u5 = sub.add_step(Justification(p("p(a) -> s(foo)"), RuleM::ForallElim, vec![i(u4.clone())], vec![])); // TODO: generalized forall?
             let u6 = sub.add_step(Justification(p("s(foo)"), RuleM::ImpElim, vec![i(u3), i(u5.clone())], vec![]));
             (u4, u5, u6)
@@ -770,8 +770,8 @@ pub fn test_complement<P: Proof>() -> (P, Vec<PjRef<P>>, Vec<PjRef<P>>) {
     let r2 = prf.add_premise(p("~A & A"));
     let r3 = prf.add_premise(p("A | ~A"));
     let r4 = prf.add_premise(p("~A | A"));
-    let r5 = prf.add_premise(p("~(forall A, A) | (forall B, B)"));
-    let r6 = prf.add_premise(p("~(forall A, A) & (forall B, B)"));
+    let r5 = prf.add_premise(p("~(forall A A) | (forall B B)"));
+    let r6 = prf.add_premise(p("~(forall A A) & (forall B B)"));
     let r19 = prf.add_premise(p("(A -> A) & (B <-> B) & (C <-> ~C) & (~D <-> D)"));
     let r7 = prf.add_step(Justification(p("_|_"), RuleM::Complement, vec![i(r1.clone())], vec![]));
     let r8 = prf.add_step(Justification(p("^|^"), RuleM::Complement, vec![i(r1)], vec![]));
@@ -914,7 +914,7 @@ pub fn test_reduction<P: Proof>() -> (P, Vec<PjRef<P>>, Vec<PjRef<P>>) {
     let p2 = prf.add_premise(p("(~~A | B) & ~A"));
     let p3 = prf.add_premise(p("(B & ~A) | A"));
     let p4 = prf.add_premise(p("~B | (A & ~~B)"));
-    let p5 = prf.add_premise(p("(forall A, (A & (~A | B))) | (~(forall A, (A & (~A | B))) & C)"));
+    let p5 = prf.add_premise(p("(forall A (A & (~A | B))) | (~(forall A (A & (~A | B))) & C)"));
     let p6 = prf.add_premise(p("B & (C | (~C & ~A))"));
     let p7 = prf.add_premise(p("A | (~A & (~~A | B))"));
     let p8 = prf.add_premise(p("D | (~A & (~~A | B))"));
@@ -923,7 +923,7 @@ pub fn test_reduction<P: Proof>() -> (P, Vec<PjRef<P>>, Vec<PjRef<P>>) {
     let r2 = prf.add_step(Justification(p("~A & B"), RuleM::Reduction, vec![i(p2.clone())], vec![]));
     let r3 = prf.add_step(Justification(p("A | B"), RuleM::Reduction, vec![i(p3.clone())], vec![]));
     let r4 = prf.add_step(Justification(p("~B | A"), RuleM::Reduction, vec![i(p4.clone())], vec![]));
-    let r5 = prf.add_step(Justification(p("(forall A, (A & B)) | C"), RuleM::Reduction, vec![i(p5)], vec![]));
+    let r5 = prf.add_step(Justification(p("(forall A (A & B)) | C"), RuleM::Reduction, vec![i(p5)], vec![]));
 
     let r6 = prf.add_step(Justification(p("A"), RuleM::Reduction, vec![i(p1)], vec![]));
     let r7 = prf.add_step(Justification(p("A | B"), RuleM::Reduction, vec![i(p2)], vec![]));
@@ -1118,7 +1118,7 @@ pub fn test_excluded_middle<P: Proof>() -> (P, Vec<PjRef<P>>, Vec<PjRef<P>>) {
     let r8 = prf.add_step(Justification(p("B"), RuleM::ExcludedMiddle, vec![], vec![]));
     let r9 = prf.add_step(Justification(p("R -> P"), RuleM::ExcludedMiddle, vec![], vec![]));
     let r10 = prf.add_step(Justification(p("R -> T"), RuleM::ExcludedMiddle, vec![], vec![]));
-    let r11 = prf.add_step(Justification(p("(A & B & C & forall P, P) | ~(A & B & C & forall P, P)"), RuleM::ExcludedMiddle, vec![], vec![]));
+    let r11 = prf.add_step(Justification(p("(A & B & C & forall P P) | ~(A & B & C & forall P P)"), RuleM::ExcludedMiddle, vec![], vec![]));
     (prf, vec![i(r1), i(r4), i(r5), i(r11)], vec![i(r2), i(r3), i(r6), i(r7), i(r8), i(r9), i(r10)])
 }
 
@@ -1127,14 +1127,14 @@ pub fn test_weak_induction<P: Proof>() -> (P, Vec<PjRef<P>>, Vec<PjRef<P>>) {
     use crate::parser::parse_unwrap as p;
     let mut prf = P::new();
     let r1 = prf.add_premise(p("~LessThan(0,0)"));
-    let r2 = prf.add_premise(p("forall x, ~LessThan(x,x) -> ~LessThan(s(x),s(x))"));
+    let r2 = prf.add_premise(p("forall x ~LessThan(x,x) -> ~LessThan(s(x),s(x))"));
     let r3 = prf.add_premise(p("Equals(0,0)"));
-    let r4 = prf.add_premise(p("forall 0, Equals(0,0) -> Equals(s(0),s(0))"));
-    let r5 = prf.add_step(Justification(p("forall x, ~LessThan(x,x)"), RuleM::WeakInduction, vec![i(r1.clone()), i(r2.clone())], vec![]));
-    let r6 = prf.add_step(Justification(p("forall x, ~LessThan(x,x)"), RuleM::WeakInduction, vec![i(r2.clone()), i(r1.clone())], vec![]));
-    let r7 = prf.add_step(Justification(p("forall n, ~LessThan(n,n)"), RuleM::WeakInduction, vec![i(r1.clone()), i(r2.clone())], vec![]));
-    let r8 = prf.add_step(Justification(p("forall x, Equals(x,x)"), RuleM::WeakInduction, vec![i(r3.clone()), i(r4.clone())], vec![]));
-    let r9 = prf.add_step(Justification(p("forall x, Equals(x,0)"), RuleM::WeakInduction, vec![i(r3.clone()), i(r4.clone())], vec![]));
+    let r4 = prf.add_premise(p("forall 0 Equals(0,0) -> Equals(s(0),s(0))"));
+    let r5 = prf.add_step(Justification(p("forall x ~LessThan(x,x)"), RuleM::WeakInduction, vec![i(r1.clone()), i(r2.clone())], vec![]));
+    let r6 = prf.add_step(Justification(p("forall x ~LessThan(x,x)"), RuleM::WeakInduction, vec![i(r2.clone()), i(r1.clone())], vec![]));
+    let r7 = prf.add_step(Justification(p("forall n ~LessThan(n,n)"), RuleM::WeakInduction, vec![i(r1.clone()), i(r2.clone())], vec![]));
+    let r8 = prf.add_step(Justification(p("forall x Equals(x,x)"), RuleM::WeakInduction, vec![i(r3.clone()), i(r4.clone())], vec![]));
+    let r9 = prf.add_step(Justification(p("forall x Equals(x,0)"), RuleM::WeakInduction, vec![i(r3.clone()), i(r4.clone())], vec![]));
     (prf, vec![i(r1), i(r2), i(r3), i(r4), i(r5), i(r6), i(r7), i(r8)], vec![i(r9)])
 }
 
@@ -1142,13 +1142,13 @@ pub fn test_strong_induction<P: Proof>() -> (P, Vec<PjRef<P>>, Vec<PjRef<P>>) {
     use self::coproduct_inject as i;
     use crate::parser::parse_unwrap as p;
     let mut prf = P::new();
-    let r1 = prf.add_premise(p("forall n, (forall x, LessThan(x, n) -> P(x)) -> P(n)"));
-    let r2 = prf.add_premise(p("forall n, (forall x, LessThan(x, n) -> P(x,n)) -> P(n,n)"));
-    let r3 = prf.add_step(Justification(p("forall x, P(x)"), RuleM::StrongInduction, vec![i(r1.clone())], vec![]));
-    let r4 = prf.add_step(Justification(p("forall n, P(n)"), RuleM::StrongInduction, vec![i(r1.clone())], vec![]));
-    let r5 = prf.add_step(Justification(p("forall n, P(n)"), RuleM::StrongInduction, vec![i(r2.clone())], vec![]));
-    let r6 = prf.add_step(Justification(p("forall x, P(x,n)"), RuleM::StrongInduction, vec![i(r1.clone())], vec![]));
-    let r7 = prf.add_step(Justification(p("forall x, P(x,n)"), RuleM::StrongInduction, vec![i(r2.clone())], vec![]));
-    let r8 = prf.add_step(Justification(p("forall a, P(a)"), RuleM::StrongInduction, vec![i(r1.clone())], vec![]));
+    let r1 = prf.add_premise(p("forall n (forall x LessThan(x, n) -> P(x)) -> P(n)"));
+    let r2 = prf.add_premise(p("forall n (forall x LessThan(x, n) -> P(x,n)) -> P(n,n)"));
+    let r3 = prf.add_step(Justification(p("forall x P(x)"), RuleM::StrongInduction, vec![i(r1.clone())], vec![]));
+    let r4 = prf.add_step(Justification(p("forall n P(n)"), RuleM::StrongInduction, vec![i(r1.clone())], vec![]));
+    let r5 = prf.add_step(Justification(p("forall n P(n)"), RuleM::StrongInduction, vec![i(r2.clone())], vec![]));
+    let r6 = prf.add_step(Justification(p("forall x P(x,n)"), RuleM::StrongInduction, vec![i(r1.clone())], vec![]));
+    let r7 = prf.add_step(Justification(p("forall x P(x,n)"), RuleM::StrongInduction, vec![i(r2.clone())], vec![]));
+    let r8 = prf.add_step(Justification(p("forall a P(a)"), RuleM::StrongInduction, vec![i(r1.clone())], vec![]));
     (prf, vec![i(r1), i(r2), i(r3), i(r4), i(r8)], vec![i(r5), i(r6), i(r7)])
 }
diff --git a/aris/src/rules.rs b/aris/src/rules.rs
index 0cbc6e4c..56e5d613 100644
--- a/aris/src/rules.rs
+++ b/aris/src/rules.rs
@@ -202,8 +202,8 @@ pub type Rule = SharedChecks<Coprod!(PrepositionalInference, PredicateInference,
 /// Conveniences for constructing rules of the appropriate type, primarily for testing.
 /// The non-standard naming conventions here are because a module is being used to pretend to be an enum.
 #[allow(non_snake_case)]
+#[allow(non_upper_case_globals)]
 pub mod RuleM {
-    #![allow(non_upper_case_globals)]
     use super::*;
     macro_rules! declare_rules {
         ($([$id:ident, $name:literal, $value:tt]),+) => {
diff --git a/bindings/java/src/java_proof.rs b/bindings/java/src/java_proof.rs
index bae78e5a..0f3fe47c 100644
--- a/bindings/java/src/java_proof.rs
+++ b/bindings/java/src/java_proof.rs
@@ -90,12 +90,12 @@ pub extern "system" fn Java_edu_rpi_aris_proof_RustProof_checkRuleAtLine(env: JN
         println!("RustProof::checkRuleAtLine {self_:?}");
         if let Some(line) = self_.lines.get(linenum as _) {
             if let Err(e) = self_.proof.verify_line(&line.reference) {
-                Ok(env.new_string(&format!("{e}"))?.into_inner())
+                Ok(env.new_string(format!("{e}"))?.into_inner())
             } else {
                 Ok(std::ptr::null_mut())
             }
         } else {
-            Ok(env.new_string(&format!("Failed to dereference line {linenum} in {self_:?}"))?.into_inner())
+            Ok(env.new_string(format!("Failed to dereference line {linenum} in {self_:?}"))?.into_inner())
         }
     })
 }
diff --git a/bindings/js/src/proofs.rs b/bindings/js/src/proofs.rs
index cc39b4fa..96900275 100644
--- a/bindings/js/src/proofs.rs
+++ b/bindings/js/src/proofs.rs
@@ -228,6 +228,7 @@ impl Proof {
 }
 
 #[wasm_bindgen]
+#[allow(dead_code)]
 pub struct Subproof(Sp);
 
 #[wasm_bindgen]
diff --git a/bindings/js/src/rules.rs b/bindings/js/src/rules.rs
index 35a62749..991b4952 100644
--- a/bindings/js/src/rules.rs
+++ b/bindings/js/src/rules.rs
@@ -12,6 +12,7 @@ pub fn rule_names() -> JsResult<Vec<JsValue>> {
 }
 
 #[wasm_bindgen]
+#[allow(dead_code)]
 pub struct Rule(aris::rules::Rule);
 
 #[wasm_bindgen]
diff --git a/web-app/src/components/proof_widget/mod.rs b/web-app/src/components/proof_widget/mod.rs
index 784fbb5f..f0ef8496 100644
--- a/web-app/src/components/proof_widget/mod.rs
+++ b/web-app/src/components/proof_widget/mod.rs
@@ -5,8 +5,6 @@ use crate::components::expr_entry::ExprEntry;
 use crate::proof_ui_data::ProofUiData;
 use crate::util::calculate_lineinfo;
 use crate::util::P;
-
-
 use aris::expr::Expr;
 use aris::proofs::pj_to_pjs;
 use aris::proofs::JsRef;
@@ -176,10 +174,10 @@ impl ProofWidget {
                     .map(|rule| {
                         let pjref = Coproduct::inject(jref);
                         // Create menu item for rule
-                        //tooltip portion addapted from: 
-                        // * https://stackoverflow.com/questions/31483302/how-to-display-an-image-inside-bootstrap-tooltip 
-                        // * https://getbootstrap.com/docs/4.1/components/tooltips/ 
-                      html! {
+                        //tooltip portion addapted from:
+                        // * https://stackoverflow.com/questions/31483302/how-to-display-an-image-inside-bootstrap-tooltip
+                        // * https://getbootstrap.com/docs/4.1/components/tooltips/
+                        html! {
                             <button class="dropdown-item" type="button" data-toggle="tooltip" data-placement="right" title={format!("<img id='rule-img' src='proofImages_light/{}.png'/>", rule.get_name())} onclick={ ctx.link().callback(move |_| ProofWidgetMsg::LineAction(LineActionKind::SetRule { rule }, pjref)) }>
                             { rule.get_name() }
                             </button>
@@ -225,7 +223,7 @@ impl ProofWidget {
         // Iterator over subproof dependency badges, for rendering list of
         // dependencies
         let sdep_badges = just.3.iter().filter_map(|sdep| self.prf.lookup_subproof(sdep)).map(|sub| {
-            let (mut lo, mut hi) = (usize::max_value(), usize::min_value());
+            let (mut lo, mut hi) = (usize::MAX, usize::MIN);
             for line in sub.premises().into_iter().map(Coproduct::inject).chain(sub.direct_lines().into_iter().map(Coproduct::inject)) {
                 if let Some((i, _)) = self.pud.ref_to_line_depth.get(&line) {
                     lo = std::cmp::min(lo, *i);