diff --git a/package.json b/package.json
index 1fe2c4d..33b2912 100644
--- a/package.json
+++ b/package.json
@@ -12,7 +12,7 @@
     "res:clean": "rescript clean",
     "res:dev": "rescript watch",
     "res:format": "rescript format",
-    "test": "npm run res:build && pta 'tests/*.mjs'",
+    "test": "pta 'tests/*.mjs'",
     "test-watch": "onchange --initial '{tests,src}/*.mjs' -- pta 'tests/*.mjs'",
     "prepare": "husky"
   },
diff --git a/src/AtomDef.res b/src/AtomDef.res
index 9f72bd1..9d29802 100644
--- a/src/AtomDef.res
+++ b/src/AtomDef.res
@@ -1,13 +1,13 @@
 // type level stuff to enable well-typed coercions
 type atomTag<_> = ..
-type rec hValue = HValue(atomTag<'a>, 'a): hValue
+type rec anyValue = HValue(atomTag<'a>, 'a): anyValue
 
 // to allow circular coercions, we declare base types
 // separately from relevant implementation
 module type BASE_ATOM = {
   type t
   type atomTag<_> += Tag: atomTag<t>
-  let wrap: t => hValue
+  let wrap: t => anyValue
 }
 
 module MakeBaseAtom = (
@@ -31,107 +31,108 @@ module type ATOM = {
   let upshift: (t, int, ~from: int=?) => t
   let substDeBruijn: (t, array<option<t>>, ~from: int=?) => t
   let concrete: t => bool
-  let coerce: hValue => option<t>
-  let wrap: t => hValue
+  let coerce: anyValue => option<t>
 }
 
 type loweredSExp = Var({idx: int}) | Schematic({schematic: int, allowed: array<int>})
 type atomTag<_> += SExpTag: atomTag<loweredSExp>
 
-exception MatchCombineAtomForeign
+exception AtomExpected
 
-module CombineAtom = (Left: ATOM, Right: ATOM): {
-  type base =
-    | Left(Left.t)
-    | Right(Right.t)
-    // strictly for coercions
-    // occurs when passed from some relative in the tree
-    // or when SExp values are lowered into loweredSExp
-    | Foreign(hValue)
-  include ATOM with type BaseAtom.t = base
-  let match: (t, Left.t => 'a, Right.t => 'a) => 'a
-} => {
-  type rec base =
-    | Left(Left.t)
-    | Right(Right.t)
-    | Foreign(hValue)
-  module BaseAtom = MakeBaseAtom({
-    type t = base
+module AtomListBase = MakeBaseAtom({
+  type t = anyValue
+})
+
+module type ATOM_LIST = {
+  module HeadBase: BASE_ATOM
+  include ATOM with module BaseAtom = AtomListBase
+  let onHead: (t, HeadBase.t => 'a) => option<'a>
+}
+
+module NilAtomList: ATOM_LIST = {
+  module HeadBase = MakeBaseAtom({
+    // empty
+    type t = {.}
   })
+  module BaseAtom = AtomListBase
+  type t = BaseAtom.t
+  type subst = Map.t<int, t>
+  let parse = (_, ~scope as _, ~gen as _=?) => Error("expected atom")
+  // ideally we could check that the tags
+  // in each argument are the same before returning Seq.empty, otherwise throw
+  // but building up a type-level witness to tag equality is not easy with the
+  // extensible variant stuff
+  let unify = (_, _, ~gen as _=?) => Seq.empty
+  // this should probably throw too, but will be more
+  // informative to have it appear wherever it's called from
+  let prettyPrint = (_, ~scope as _) => "NIL (THIS IS AN ERROR!)"
+  let onHead = (_, _) => throw(AtomExpected)
+  let coerce = _ => throw(AtomExpected)
+  let substitute = (_, _) => throw(AtomExpected)
+  let upshift = (_, _, ~from as _=?) => throw(AtomExpected)
+  let substDeBruijn = (_, _, ~from as _=?) => throw(AtomExpected)
+  let concrete = _ => throw(AtomExpected)
+}
+
+module CombineAtom = (Head: ATOM, Tail: ATOM_LIST): (
+  ATOM_LIST with module HeadBase = Head.BaseAtom
+) => {
+  module HeadBase = Head.BaseAtom
+  module Tail = Tail
+  module BaseAtom = AtomListBase
   type t = BaseAtom.t
   type subst = Map.t<int, t>
   type gen = ref<int>
-  let coerce = v => Some(Foreign(v))
-  let match = (t, leftBranch: Left.t => 'a, rightBranch: Right.t => 'a): 'a =>
-    switch t {
-    | Left(s) => leftBranch(s)
-    | Right(s) => rightBranch(s)
-    | Foreign(_) => throw(MatchCombineAtomForeign)
-    }
-  let wrap = t =>
-    switch t {
-    | Left(s) => Left.wrap(s)
-    | Right(s) => Right.wrap(s)
-    | Foreign(val) => val
+  let getOrElse = Util.Option.getOrElse
+  let coerce = v => Some(v)
+  let onHead = (HValue(tag, val), f: Head.t => 'a): option<'a> =>
+    switch tag {
+    | Head.BaseAtom.Tag => Some(f(val))
+    | _ => None
     }
   let parse = (s, ~scope, ~gen: option<gen>=?) => {
-    Left.parse(s, ~scope, ~gen?)
-    ->Result.map(((r, rest)) => (Left(r), rest))
-    ->Util.Result.or(() =>
-      Right.parse(s, ~scope, ~gen?)->Result.map(((r, rest)) => (Right(r), rest))
-    )
+    Head.parse(s, ~scope, ~gen?)
+    ->Result.map(((r, rest)) => (HeadBase.wrap(r), rest))
+    ->Util.Result.or(() => Tail.parse(s, ~scope, ~gen?))
   }
-  let prettyPrint = (s, ~scope) =>
-    s->match(left => Left.prettyPrint(left, ~scope), right => Right.prettyPrint(right, ~scope))
-  let unify = (s1, s2, ~gen=?) =>
-    switch (s1, s2) {
-    | (Left(s1), Left(s2)) =>
-      Left.unify(s1, s2, ~gen?)->Seq.map(subst => subst->Util.mapMapValues(v => Left(v)))
-    | (Right(s1), Right(s2)) =>
-      Right.unify(s1, s2, ~gen?)->Seq.map(subst => subst->Util.mapMapValues(v => Right(v)))
-    | (_, _) => Seq.empty
-    }
-  let coerceToLeft = (t): option<Left.t> =>
-    switch t {
-    | Left(s) => Some(s)
-    | Right(s) => Right.wrap(s)->Left.coerce
-    | Foreign(v) => Left.coerce(v)
-    }
-  let coerceToRight = (t): option<Right.t> =>
-    switch t {
-    | Right(s) => Some(s)
-    | Left(s) => Left.wrap(s)->Right.coerce
-    | Foreign(v) => Right.coerce(v)
+  let prettyPrint = (atom, ~scope) =>
+    atom
+    ->onHead(val => Head.prettyPrint(val, ~scope))
+    ->getOrElse(() => Tail.prettyPrint(atom, ~scope))
+
+  let unify = (a1, a2, ~gen=?) => {
+    let (HValue(tag1, val1), HValue(tag2, val2)) = (a1, a2)
+    switch (tag1, tag2) {
+    | (Head.BaseAtom.Tag, Head.BaseAtom.Tag) =>
+      Head.unify(val1, val2)->Seq.map(subst => subst->Util.mapMapValues(HeadBase.wrap))
+    | (_, _) => Tail.unify(a1, a2, ~gen?)
     }
-  let substitute = (s, subst: subst) => {
-    s->match(
-      left => {
-        let leftSubs = subst->Util.Map.filterMap((_, v) => coerceToLeft(v))
-        Left(Left.substitute(left, leftSubs))
-      },
-      right => {
-        let rightSubs = subst->Util.Map.filterMap((_, v) => coerceToRight(v))
-        Right(Right.substitute(right, rightSubs))
-      },
-    )
   }
-  let upshift = (s, amount: int, ~from=?) =>
-    s->match(
-      left => Left(left->Left.upshift(amount, ~from?)),
-      right => Right(right->Right.upshift(amount, ~from?)),
-    )
-  let substDeBruijn = (s, substs: array<option<t>>, ~from=?) =>
-    s->match(
-      left => {
-        let leftSubs = substs->Array.map(o => o->Option.flatMap(coerceToLeft))
-        Left(Left.substDeBruijn(left, leftSubs, ~from?))
-      },
-      right => {
-        let rightSubs = substs->Array.map(o => o->Option.flatMap(coerceToRight))
-        Right(Right.substDeBruijn(right, rightSubs, ~from?))
-      },
+  let coerceToHead = (atom): option<Head.t> =>
+    atom->onHead(val => Some(val))->getOrElse(() => Head.coerce(atom))
+  let substitute = (atom, subst: subst) =>
+    atom
+    ->onHead(val => {
+      let leftSubs = subst->Util.Map.filterMap((_, v) => coerceToHead(v))
+      Head.substitute(val, leftSubs)->HeadBase.wrap
+    })
+    ->getOrElse(() => Tail.substitute(atom, subst))
+
+  let upshift = (atom, amount: int, ~from=?) =>
+    atom
+    ->onHead(val => Head.upshift(val, amount, ~from?)->HeadBase.wrap)
+    ->getOrElse(() => Tail.upshift(atom, amount, ~from?))
+  let substDeBruijn = (atom, substs: array<option<t>>, ~from=?) =>
+    atom
+    ->onHead(val =>
+      Head.substDeBruijn(
+        val,
+        substs->Array.map(o => o->Option.flatMap(coerceToHead)),
+        ~from?,
+      )->HeadBase.wrap
     )
-  let concrete = s => s->match(Left.concrete, Right.concrete)
+    ->getOrElse(() => Tail.substDeBruijn(atom, substs, ~from?))
+  let concrete = atom => atom->onHead(Head.concrete)->getOrElse(() => Tail.concrete(atom))
 }
 
 module type ATOM_VIEW = {
@@ -140,27 +141,29 @@ module type ATOM_VIEW = {
   let make: props => React.element
 }
 
+module NilAtomListView: ATOM_VIEW with module Atom := NilAtomList = {
+  type props = {name: NilAtomList.t, scope: array<string>}
+  let make = _ => throw(AtomExpected)
+}
+
 module MakeAtomView = (
   Left: ATOM,
   LeftView: ATOM_VIEW with module Atom := Left,
-  Right: ATOM,
+  Right: ATOM_LIST,
   RightView: ATOM_VIEW with module Atom := Right,
   Combined: module type of CombineAtom(Left, Right),
-): {
-  include ATOM_VIEW with module Atom := Combined
-} => {
+): (ATOM_VIEW with module Atom := Combined) => {
   type props = {name: Combined.t, scope: array<string>}
   let make = ({name, scope}: props) =>
-    name->Combined.match(
-      left => <LeftView name={left} scope />,
-      right => <RightView name={right} scope />,
-    )
+    name
+    ->Combined.onHead(left => <LeftView name={left} scope />)
+    ->Util.Option.getOrElse(() => <RightView name scope />)
 }
 
 module MakeAtomAndView = (
   Left: ATOM,
   LeftView: ATOM_VIEW with module Atom := Left,
-  Right: ATOM,
+  Right: ATOM_LIST,
   RightView: ATOM_VIEW with module Atom := Right,
 ) => {
   module Atom = CombineAtom(Left, Right)
diff --git a/src/RuleView.res b/src/RuleView.res
index ae9b631..00ca9ee 100644
--- a/src/RuleView.res
+++ b/src/RuleView.res
@@ -1,5 +1,5 @@
 open Signatures
-open Util
+open! Util
 type style = Gentzen | Linear | Hybrid
 module Make = (
   Term: TERM,
diff --git a/src/Scratch.res b/src/Scratch.res
index 5bc2d8d..6086d15 100644
--- a/src/Scratch.res
+++ b/src/Scratch.res
@@ -42,11 +42,17 @@ module DLREView = MethodView.CombineMethodView(
 module TheoremS = Editable.TextArea(Theorem.Make(HOTerm, HOTerm, HOTermJView, DLRView))
 module ConfS = ConfigBlock.Make(HOTerm, HOTerm)
 
+module Symbol = AtomDef.MakeAtomAndView(
+  Symbolic.Atom,
+  Symbolic.AtomView,
+  AtomDef.NilAtomList,
+  AtomDef.NilAtomListView,
+)
 module StringSymbol = AtomDef.MakeAtomAndView(
   StringA.Atom,
   StringA.AtomView,
-  Symbolic.Atom,
-  Symbolic.AtomView,
+  Symbol.Atom,
+  Symbol.AtomView,
 )
 module StringSExp = SExp.Make(StringSymbol.Atom)
 module TermView = SExpView.Make(StringSymbol.Atom, StringSymbol.AtomView, StringSExp)
diff --git a/src/StringA.res b/src/StringA.res
index f60e849..c8b6d7c 100644
--- a/src/StringA.res
+++ b/src/StringA.res
@@ -478,7 +478,6 @@ module Atom = {
       ])
     | _ => None
     }
-  let wrap = a => AtomDef.HValue(BaseAtom.Tag, a)
 }
 
 module AtomView = {
diff --git a/src/StringAxiomSet.res b/src/StringAxiomSet.res
index 8019ae1..35905a1 100644
--- a/src/StringAxiomSet.res
+++ b/src/StringAxiomSet.res
@@ -1,11 +1,19 @@
 open Component
+open! Util
 
+module Symbol = AtomDef.MakeAtomAndView(
+  Symbolic.Atom,
+  Symbolic.AtomView,
+  AtomDef.NilAtomList,
+  AtomDef.NilAtomListView,
+)
 module StringSymbol = AtomDef.MakeAtomAndView(
   StringA.Atom,
   StringA.AtomView,
-  Symbolic.Atom,
-  Symbolic.AtomView,
+  Symbol.Atom,
+  Symbol.AtomView,
 )
+
 module StringSExp = SExp.Make(StringSymbol.Atom)
 module TermView = SExpView.Make(StringSymbol.Atom, StringSymbol.AtomView, StringSExp)
 module JudgmentView = TermViewAsJudgmentView.Make(StringSExp, StringSExp, TermView)
@@ -42,16 +50,18 @@ let getSExpName = (t: StringSExp.t): option<string> =>
   | _ => None
   }
 
-let destructure = (r: StringSExp.t): (StringA.Atom.t, string) =>
-  switch r {
-  | Compound({subexps: [Atom(Left(s)), Atom(Right(name))]}) => (s, name)
-  | _ => throw(Util.Unreachable("expected valid induction rule"))
-  }
 let destructureOpt = (r: StringSExp.t): option<(StringA.Atom.t, string)> =>
   switch r {
-  | Compound({subexps: [Atom(Left(s)), Atom(Right(name))]}) => Some((s, name))
+  | Compound({subexps: [Atom(AtomDef.HValue(tag1, s)), Atom(AtomDef.HValue(tag2, name))]}) =>
+    switch (tag1, tag2) {
+    | (StringA.BaseAtom.Tag, Symbolic.BaseAtom.Tag) => Some((s, name))
+    | _ => None
+    }
   | _ => None
   }
+exception InvalidStringInductionPattern
+let destructure = (r: StringSExp.t): (StringA.Atom.t, string) =>
+  destructureOpt(r)->Option.getOrElse(() => throw(InvalidStringInductionPattern))
 let structure = (lhs: StringSExp.t, rhs: StringSExp.t): StringSExp.t => Compound({
   subexps: [lhs, rhs],
 })
@@ -114,7 +124,7 @@ let derive = (group: judgeGroup, mentionedGroups: array<judgeGroup>): Rule.t =>
       vars: rule.vars,
       premises: rule.premises->Array.concat(inductionHyps),
       conclusion: structure(
-        surround(s, aIdx + baseIdx, bIdx + baseIdx)->Left->Atom,
+        Atom(AtomDef.HValue(StringA.BaseAtom.Tag, surround(s, aIdx + baseIdx, bIdx + baseIdx))),
         Var({idx: pIdx + baseIdx}),
       ),
     }
@@ -126,13 +136,16 @@ let derive = (group: judgeGroup, mentionedGroups: array<judgeGroup>): Rule.t =>
         {
           Rule.vars: [],
           premises: [],
-          conclusion: structure(Var({idx: xIdx}), Atom(Right(group.name))),
+          conclusion: structure(
+            Var({idx: xIdx}),
+            Atom(AtomDef.HValue(Symbolic.BaseAtom.Tag, group.name)),
+          ),
         },
       ],
       mentionedGroups->Array.flatMap(g => g.rules->Array.map(r => replaceJudgeRHS(r, 0))),
     ),
     conclusion: structure(
-      surround([StringA.Var({idx: xIdx})], aIdx, bIdx)->Left->Atom,
+      Atom(HValue(StringA.BaseAtom.Tag, surround([StringA.Var({idx: xIdx})], aIdx, bIdx))),
       Var({idx: 0}),
     ), // TODO: clean here
   }
@@ -170,8 +183,8 @@ let deserialise = (str: string, ~imports as _: Ports.t) => {
   getBase(str)->Result.map(raw => {
     let grouped: dict<array<Rule.t>> = Dict.make()
     raw->Dict.forEach(rule =>
-      switch rule.conclusion {
-      | Compound({subexps: [Atom(Left(_)), Atom(Right(name))]}) =>
+      switch rule.conclusion->destructureOpt {
+      | Some((_, name)) =>
         switch grouped->Dict.get(name) {
         | None => grouped->Dict.set(name, [rule])
         | Some(rs) => rs->Array.push(rule)
diff --git a/src/Util.res b/src/Util.res
index 30daf04..4cdef54 100644
--- a/src/Util.res
+++ b/src/Util.res
@@ -143,14 +143,25 @@ let mustFindIndex = (arr, f) => {
 }
 
 module Result = {
-  let ok = (r: result<'a, 'b>): option<'a> =>
+  include Result
+  type t<'a, 'b> = result<'a, 'b>
+  let ok = (r: t<'a, 'b>): option<'a> =>
     switch r {
     | Ok(a) => Some(a)
     | Error(_) => None
     }
-  let or = (r1: result<'a, 'b>, r2: unit => result<'a, 'b>): result<'a, 'b> =>
+  let or = (r1: t<'a, 'b>, r2: unit => t<'a, 'b>): t<'a, 'b> =>
     switch r1 {
     | Ok(_) => r1
     | Error(_) => r2()
     }
 }
+
+module Option = {
+  include Option
+  let getOrElse = (t, f): 'a =>
+    switch t {
+    | Some(a) => a
+    | None => f()
+    }
+}
diff --git a/tests/RuleTest.res b/tests/RuleTest.res
index c4a721a..abccc2d 100644
--- a/tests/RuleTest.res
+++ b/tests/RuleTest.res
@@ -32,13 +32,21 @@ module MakeTest = (Term: TERM, Judgment: JUDGMENT with module Term := Term) => {
 }
 
 zoraBlock("string terms", t => {
+  module Symbol = AtomDef.MakeAtomAndView(
+    Symbolic.Atom,
+    Symbolic.AtomView,
+    AtomDef.NilAtomList,
+    AtomDef.NilAtomListView,
+  )
   module StringSymbol = AtomDef.MakeAtomAndView(
     StringA.Atom,
     StringA.AtomView,
-    Symbolic.Atom,
-    Symbolic.AtomView,
+    Symbol.Atom,
+    Symbol.AtomView,
   )
   module StringSExp = SExp.Make(StringSymbol.Atom)
+  let wrapString = (s): StringSExp.t => Atom(AtomDef.HValue(StringA.BaseAtom.Tag, s))
+  let wrapSymbol = (s): StringSExp.t => Atom(HValue(Symbolic.BaseAtom.Tag, s))
   module T = MakeTest(StringSExp, StringSExp)
   t->T.testParseInner(
     `[s1. ("$s1" p) |- ("($s1)" p)]`,
@@ -49,19 +57,14 @@ zoraBlock("string terms", t => {
           vars: [],
           premises: [],
           conclusion: StringSExp.Compound({
-            subexps: [
-              [StringA.Var({idx: 0})]->StringSymbol.Atom.Left->StringSExp.Atom,
-              "p"->StringSymbol.Atom.Right->StringSExp.Atom,
-            ],
+            subexps: [wrapString([StringA.Var({idx: 0})]), wrapSymbol("p")],
           }),
         },
       ],
       conclusion: StringSExp.Compound({
         subexps: [
-          [StringA.String("("), StringA.Var({idx: 0}), StringA.String(")")]
-          ->StringSymbol.Atom.Left
-          ->StringSExp.Atom,
-          "p"->StringSymbol.Atom.Right->StringSExp.Atom,
+          wrapString([StringA.String("("), StringA.Var({idx: 0}), StringA.String(")")]),
+          wrapSymbol("p"),
         ],
       }),
     },