diff --git a/src/AtomBase.res b/src/AtomBase.res
new file mode 100644
index 0000000..6668c29
--- /dev/null
+++ b/src/AtomBase.res
@@ -0,0 +1,34 @@
+// type level stuff to enable well-typed coercions
+type atomTag<_> = ..
+type rec anyValue = AnyValue(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 => anyValue
+}
+
+module Make = (
+  T: {
+    type t
+  },
+): (BASE_ATOM with type t = T.t) => {
+  type t = T.t
+  type atomTag<_> += Tag: atomTag<t>
+  let wrap = t => AnyValue(Tag, t)
+}
+
+module String = {
+  type piece =
+    | String(string)
+    | Var({idx: int})
+    | Schematic({schematic: int, allowed: array<int>})
+  include Make({type t = array<piece>})
+}
+
+module VarBase = {
+  type varBase = Var({idx: int}) | Schematic({schematic: int, allowed: array<int>})
+  include Make({type t = varBase})
+}
diff --git a/src/AtomDef.res b/src/AtomDef.res
index 9c028cc..fff14f3 100644
--- a/src/AtomDef.res
+++ b/src/AtomDef.res
@@ -1,28 +1,8 @@
-// type level stuff to enable well-typed coercions
-type atomTag<_> = ..
-type rec anyValue = AnyValue(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 => anyValue
-}
-
-module MakeBaseAtom = (
-  T: {
-    type t
-  },
-): (BASE_ATOM with type t = T.t) => {
-  type t = T.t
-  type atomTag<_> += Tag: atomTag<t>
-  let wrap = t => AnyValue(Tag, t)
-}
+open AtomBase
 
 module type ATOM = {
-  module BaseAtom: BASE_ATOM
-  type t = BaseAtom.t
+  module Base: BASE_ATOM
+  type t = Base.t
   type subst = Map.t<int, t>
   let unify: (t, t, ~gen: ref<int>=?) => Seq.t<subst>
   let prettyPrint: (t, ~scope: array<string>) => string
@@ -34,41 +14,32 @@ module type ATOM = {
   let coerce: anyValue => option<t>
 }
 
-type varBase = Var({idx: int}) | Schematic({schematic: int, allowed: array<int>})
-module VarBase = MakeBaseAtom({
-  type t = varBase
-})
-
 exception AtomExpected
 
-module AtomListBase = MakeBaseAtom({
+module AtomChoiceBase = Make({
   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 type ATOM_CHOICE = {
+  module LeftBase: BASE_ATOM
+  include ATOM with module Base = AtomChoiceBase
+  let onLeft: (t, LeftBase.t => 'a) => option<'a>
 }
 
-module NilAtomList: ATOM_LIST = {
-  module HeadBase = MakeBaseAtom({
+module EmptyAtomChoice: ATOM_CHOICE = {
+  module LeftBase = AtomBase.Make({
     // empty
     type t = {.}
   })
-  module BaseAtom = AtomListBase
-  type t = BaseAtom.t
+  module Base = AtomChoiceBase
+  type t = Base.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 onLeft = (_, _) => throw(AtomExpected)
   let coerce = _ => throw(AtomExpected)
   let substitute = (_, _) => throw(AtomExpected)
   let upshift = (_, _, ~from as _=?) => throw(AtomExpected)
@@ -76,98 +47,98 @@ module NilAtomList: ATOM_LIST = {
   let concrete = _ => throw(AtomExpected)
 }
 
-module CombineAtom = (Head: ATOM, Tail: ATOM_LIST): (
-  ATOM_LIST with module HeadBase = Head.BaseAtom
+module MakeAtomChoice = (Left: ATOM, Right: ATOM_CHOICE): (
+  ATOM_CHOICE with module LeftBase = Left.Base
 ) => {
-  module HeadBase = Head.BaseAtom
-  module Tail = Tail
-  module BaseAtom = AtomListBase
-  type t = BaseAtom.t
+  module LeftBase = Left.Base
+  module Right = Right
+  module Base = AtomChoiceBase
+  type t = Base.t
   type subst = Map.t<int, t>
   type gen = ref<int>
   let getOrElse = Util.Option.getOrElse
   let coerce = v => Some(v)
-  let onHead = (AnyValue(tag, val), f: Head.t => 'a): option<'a> =>
+  let onLeft = (AnyValue(tag, val), f: Left.t => 'a): option<'a> =>
     switch tag {
-    | Head.BaseAtom.Tag => Some(f(val))
+    | Left.Base.Tag => Some(f(val))
     | _ => None
     }
   let parse = (s, ~scope, ~gen: option<gen>=?) => {
-    Head.parse(s, ~scope, ~gen?)
-    ->Result.map(((r, rest)) => (HeadBase.wrap(r), rest))
-    ->Util.Result.or(() => Tail.parse(s, ~scope, ~gen?))
+    Left.parse(s, ~scope, ~gen?)
+    ->Result.map(((r, rest)) => (LeftBase.wrap(r), rest))
+    ->Util.Result.or(() => Right.parse(s, ~scope, ~gen?))
   }
   let prettyPrint = (atom, ~scope) =>
     atom
-    ->onHead(val => Head.prettyPrint(val, ~scope))
-    ->getOrElse(() => Tail.prettyPrint(atom, ~scope))
+    ->onLeft(val => Left.prettyPrint(val, ~scope))
+    ->getOrElse(() => Right.prettyPrint(atom, ~scope))
 
   let unify = (a1, a2, ~gen=?) => {
     let (AnyValue(tag1, val1), AnyValue(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?)
+    | (Left.Base.Tag, Left.Base.Tag) =>
+      Left.unify(val1, val2)->Seq.map(subst => subst->Util.mapMapValues(LeftBase.wrap))
+    | (_, _) => Right.unify(a1, a2, ~gen?)
     }
   }
-  let coerceToHead = (atom): option<Head.t> =>
-    atom->onHead(val => Some(val))->getOrElse(() => Head.coerce(atom))
+  let coerceToLeft = (atom): option<Left.t> =>
+    atom->onLeft(val => Some(val))->getOrElse(() => Left.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
+    ->onLeft(val => {
+      let leftSubs = subst->Util.Map.filterMap((_, v) => coerceToLeft(v))
+      Left.substitute(val, leftSubs)->LeftBase.wrap
     })
-    ->getOrElse(() => Tail.substitute(atom, subst))
+    ->getOrElse(() => Right.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?))
+    ->onLeft(val => Left.upshift(val, amount, ~from?)->LeftBase.wrap)
+    ->getOrElse(() => Right.upshift(atom, amount, ~from?))
   let substDeBruijn = (atom, substs: array<option<t>>, ~from=?) =>
     atom
-    ->onHead(val =>
-      Head.substDeBruijn(
+    ->onLeft(val =>
+      Left.substDeBruijn(
         val,
-        substs->Array.map(o => o->Option.flatMap(coerceToHead)),
+        substs->Array.map(o => o->Option.flatMap(coerceToLeft)),
         ~from?,
-      )->HeadBase.wrap
+      )->LeftBase.wrap
     )
-    ->getOrElse(() => Tail.substDeBruijn(atom, substs, ~from?))
-  let concrete = atom => atom->onHead(Head.concrete)->getOrElse(() => Tail.concrete(atom))
+    ->getOrElse(() => Right.substDeBruijn(atom, substs, ~from?))
+  let concrete = atom => atom->onLeft(Left.concrete)->getOrElse(() => Right.concrete(atom))
 }
 
 module type ATOM_VIEW = {
   module Atom: ATOM
-  type props = {name: Atom.t, scope: array<string>}
+  type props = {atom: Atom.t, scope: array<string>}
   let make: props => React.element
 }
 
-module NilAtomListView: ATOM_VIEW with module Atom := NilAtomList = {
-  type props = {name: NilAtomList.t, scope: array<string>}
+module EmptyAtomChoiceView: ATOM_VIEW with module Atom := EmptyAtomChoice = {
+  type props = {atom: EmptyAtomChoice.t, scope: array<string>}
   let make = _ => throw(AtomExpected)
 }
 
-module MakeAtomView = (
+module MakeAtomChoiceView = (
   Left: ATOM,
   LeftView: ATOM_VIEW with module Atom := Left,
-  Right: ATOM_LIST,
+  Right: ATOM_CHOICE,
   RightView: ATOM_VIEW with module Atom := Right,
-  Combined: module type of CombineAtom(Left, Right),
+  Combined: module type of MakeAtomChoice(Left, Right),
 ): (ATOM_VIEW with module Atom := Combined) => {
-  type props = {name: Combined.t, scope: array<string>}
-  let make = ({name, scope}: props) =>
-    name
-    ->Combined.onHead(left => <LeftView name={left} scope />)
-    ->Util.Option.getOrElse(() => <RightView name scope />)
+  type props = {atom: Combined.t, scope: array<string>}
+  let make = ({atom, scope}: props) =>
+    atom
+    ->Combined.onLeft(left => <LeftView atom={left} scope />)
+    ->Util.Option.getOrElse(() => <RightView atom scope />)
 }
 
-module MakeAtomAndView = (
+module MakeAtomChoiceAndView = (
   Left: ATOM,
   LeftView: ATOM_VIEW with module Atom := Left,
-  Right: ATOM_LIST,
+  Right: ATOM_CHOICE,
   RightView: ATOM_VIEW with module Atom := Right,
 ) => {
-  module Atom = CombineAtom(Left, Right)
-  module AtomView = MakeAtomView(Left, LeftView, Right, RightView, Atom)
+  module Atom = MakeAtomChoice(Left, Right)
+  module AtomView = MakeAtomChoiceView(Left, LeftView, Right, RightView, Atom)
 }
diff --git a/src/HOTerm.res b/src/HOTerm.res
index e97afa6..899e102 100644
--- a/src/HOTerm.res
+++ b/src/HOTerm.res
@@ -6,7 +6,7 @@ module IntCmp = Belt.Id.MakeComparable({
 module type ATOM = AtomDef.ATOM
 
 module DefaultAtom = {
-  module BaseAtom = AtomDef.MakeBaseAtom({
+  module Base = AtomBase.Make({
     type t = string
   })
   type t = string
diff --git a/src/SExp.res b/src/SExp.res
index 9e481f1..f11e681 100644
--- a/src/SExp.res
+++ b/src/SExp.res
@@ -150,9 +150,9 @@ module Make = (Atom: AtomDef.ATOM): {
   let rec lower = (term: t): option<Atom.t> =>
     switch term {
     | Atom(s) => Some(s)
-    | Var({idx}) => Atom.coerce(AtomDef.VarBase.wrap(Var({idx: idx})))
+    | Var({idx}) => Atom.coerce(AtomBase.VarBase.wrap(Var({idx: idx})))
     | Schematic({schematic, allowed}) =>
-      Atom.coerce(AtomDef.VarBase.wrap(Schematic({schematic, allowed})))
+      Atom.coerce(AtomBase.VarBase.wrap(Schematic({schematic, allowed})))
     | Compound({subexps: [e1]}) => lower(e1)
     | _ => None
     }
diff --git a/src/SExpView.res b/src/SExpView.res
index 32d38fc..ee75ae6 100644
--- a/src/SExpView.res
+++ b/src/SExpView.res
@@ -55,9 +55,9 @@ module Make = (
         ->React.array}
       </span>
     | Var({idx}) => viewVar({idx, scope})
-    | Atom(name) =>
+    | Atom(atom) =>
       <span className="term-const">
-        <AtomView name scope />
+        <AtomView atom scope />
       </span>
     | Schematic({schematic: s, allowed: vs}) =>
       <span className="term-schematic">
diff --git a/src/Scratch.res b/src/Scratch.res
index c96855d..b074b11 100644
--- a/src/Scratch.res
+++ b/src/Scratch.res
@@ -42,13 +42,13 @@ module DLREView = MethodView.CombineMethodView(
 module TheoremS = Editable.TextArea(Theorem.Make(HOTerm, HOTerm, HOTermJView, DLRView))
 module ConfS = ConfigBlock.Make(HOTerm, HOTerm)
 
-module Symbol = AtomDef.MakeAtomAndView(
+module Symbol = AtomDef.MakeAtomChoiceAndView(
   Symbolic.Atom,
   Symbolic.AtomView,
-  AtomDef.NilAtomList,
-  AtomDef.NilAtomListView,
+  AtomDef.EmptyAtomChoice,
+  AtomDef.EmptyAtomChoiceView,
 )
-module StringSymbol = AtomDef.MakeAtomAndView(
+module StringSymbol = AtomDef.MakeAtomChoiceAndView(
   StringA.Atom,
   StringA.AtomView,
   Symbol.Atom,
diff --git a/src/StringA.res b/src/StringA.res
index 1dcfd4d..de4c894 100644
--- a/src/StringA.res
+++ b/src/StringA.res
@@ -3,21 +3,16 @@ module IntCmp = Belt.Id.MakeComparable({
   let cmp = Pervasives.compare
 })
 
-type piece =
-  | String(string)
-  | Var({idx: int})
-  | Schematic({schematic: int, allowed: array<int>})
-type t = array<piece>
-type meta = string
-type schematic = int
-
-module BaseAtom = AtomDef.MakeBaseAtom({
-  type t = t
-})
+module Base = AtomBase.String
+type t = Base.t
+type piece = Base.piece
 
 module Atom = {
-  module BaseAtom = BaseAtom
-  type t = t
+  module Base = Base
+  type t = Base.t
+  type schematic = int
+  type meta = string
+
   type subst = Map.t<schematic, t>
   let substitute = (term: t, subst: subst) =>
     Array.flatMap(term, piece => {
@@ -101,7 +96,7 @@ module Atom = {
       | (_, _) => {
           let (s1, ss) = uncons(s)
           switch s1 {
-          | Schematic({schematic, allowed}) =>
+          | Base.Schematic({schematic, allowed}) =>
             Belt.Array.range(0, Array.length(t))
             ->Array.map(i => {
               let subTerm = Array.slice(t, ~start=0, ~end=i)
@@ -155,7 +150,7 @@ module Atom = {
           let searchSub = (schematic: int, allowed: array<int>, edge: graphSub): array<
             array<(int, graphSub)>,
           > => {
-            let piece = Schematic({schematic, allowed})
+            let piece = Base.Schematic({schematic, allowed})
             let sub = switch edge {
             | Eps => singletonSubst(schematic, [])
             | PieceLitSub(p) => singletonSubst(schematic, [p, piece])
@@ -383,7 +378,7 @@ module Atom = {
       switch execRe(identRegex)
       ->Option.orElse(execRe(symbolRegex))
       ->Option.orElse(execRe(numberRegex)) {
-      | Some([match], l) => add(String(match), ~nAdvance=l)
+      | Some([match], l) => add(Base.String(match), ~nAdvance=l)
       | Some(_) => error("regex string lit error")
       | None => error("expected string")
       }
@@ -462,14 +457,14 @@ module Atom = {
   let concrete = t =>
     t->Array.every(p =>
       switch p {
-      | Schematic(_) => false
+      | Base.Schematic(_) => false
       | _ => true
       }
     )
-  let coerce = (AtomDef.AnyValue(tag, a)) =>
+  let coerce = (AtomBase.AnyValue(tag, a)) =>
     switch tag {
-    | Symbolic.BaseAtom.Tag => Some([String(a)])
-    | AtomDef.VarBase.Tag =>
+    | Symbolic.Base.Tag => Some([Base.String(a)])
+    | AtomBase.VarBase.Tag =>
       Some([
         switch a {
         | Var({idx}) => Var({idx: idx})
@@ -481,7 +476,7 @@ module Atom = {
 }
 
 module AtomView = {
-  type props = {name: t, scope: array<string>}
+  type props = {atom: t, scope: array<string>}
   type idx_props = {idx: int, scope: array<string>}
   let viewVar = (props: idx_props) =>
     switch props.scope[props.idx] {
@@ -527,10 +522,10 @@ module AtomView = {
   }
 
   @react.componentWithProps
-  let make = ({name, scope}) =>
+  let make = ({atom, scope}) =>
     <span className="term-compound">
       {React.string("\"")}
-      {name
+      {atom
       ->Array.mapWithIndex((piece, i) => {
         let key = Int.toString(i)
         <Piece piece scope key />
diff --git a/src/StringA.resi b/src/StringA.resi
index 192b5b8..d4a7ef2 100644
--- a/src/StringA.resi
+++ b/src/StringA.resi
@@ -1,9 +1,5 @@
-type rec piece =
-  | String(string)
-  | Var({idx: int})
-  | Schematic({schematic: int, allowed: array<int>})
-type t = array<piece>
+type t = AtomBase.String.t
 
-module BaseAtom: AtomDef.BASE_ATOM with type t = t
-module Atom: AtomDef.ATOM with module BaseAtom = BaseAtom
+module Base: AtomBase.BASE_ATOM with type t = t
+module Atom: AtomDef.ATOM with module Base = Base
 module AtomView: AtomDef.ATOM_VIEW with module Atom := Atom
diff --git a/src/StringAxiomSet.res b/src/StringAxiomSet.res
index b45b6ef..d7f8fcc 100644
--- a/src/StringAxiomSet.res
+++ b/src/StringAxiomSet.res
@@ -2,7 +2,7 @@ open Component
 open! Util
 
 module Make = (
-  Atom: AtomDef.ATOM_LIST,
+  Atom: AtomDef.ATOM_CHOICE,
   Term: module type of SExp.Make(Atom),
   JudgmentView: Signatures.JUDGMENT_VIEW with module Term := Term and module Judgment := Term,
 ) => {
@@ -34,9 +34,11 @@ module Make = (
 
   let destructureOpt = (r: Term.t): option<(StringA.Atom.t, Symbolic.Atom.t)> =>
     switch r {
-    | Compound({subexps: [Atom(AtomDef.AnyValue(tag1, s)), Atom(AtomDef.AnyValue(tag2, name))]}) =>
+    | Compound({
+        subexps: [Atom(AtomBase.AnyValue(tag1, s)), Atom(AtomBase.AnyValue(tag2, name))],
+      }) =>
       switch (tag1, tag2) {
-      | (StringA.BaseAtom.Tag, Symbolic.BaseAtom.Tag) => Some((s, name))
+      | (StringA.Base.Tag, Symbolic.Base.Tag) => Some((s, name))
       | _ => None
       }
     | _ => None
@@ -85,7 +87,10 @@ module Make = (
     let aIdx = vars->Array.findIndex(i => i == a)
     let bIdx = vars->Array.findIndex(i => i == b)
     let surround = (t: StringA.Atom.t, aIdx: int, bIdx: int) => {
-      Array.concat(Array.concat([StringA.Var({idx: aIdx})], t), [StringA.Var({idx: bIdx})])
+      Array.concat(
+        Array.concat([AtomBase.String.Var({idx: aIdx})], t),
+        [AtomBase.String.Var({idx: bIdx})],
+      )
     }
     let lookupGroup = (name: string): option<int> =>
       mentionedGroups->Array.findIndexOpt(g => name == g.name)
@@ -106,7 +111,7 @@ module Make = (
         vars: rule.vars,
         premises: rule.premises->Array.concat(inductionHyps),
         conclusion: structure(
-          Atom(surround(s, aIdx + baseIdx, bIdx + baseIdx)->StringA.BaseAtom.wrap),
+          Atom(surround(s, aIdx + baseIdx, bIdx + baseIdx)->StringA.Base.wrap),
           Var({idx: pIdx + baseIdx}),
         ),
       }
@@ -118,13 +123,13 @@ module Make = (
           {
             Rule.vars: [],
             premises: [],
-            conclusion: structure(Var({idx: xIdx}), Atom(group.name->Symbolic.BaseAtom.wrap)),
+            conclusion: structure(Var({idx: xIdx}), Atom(group.name->Symbolic.Base.wrap)),
           },
         ],
         mentionedGroups->Array.flatMap(g => g.rules->Array.map(r => replaceJudgeRHS(r, 0))),
       ),
       conclusion: structure(
-        Atom(surround([Var({idx: xIdx})], aIdx, bIdx)->StringA.BaseAtom.wrap),
+        Atom(surround([Var({idx: xIdx})], aIdx, bIdx)->StringA.Base.wrap),
         Var({idx: 0}),
       ), // TODO: clean here
     }
diff --git a/src/Symbolic.res b/src/Symbolic.res
index e3a059a..cf40c66 100644
--- a/src/Symbolic.res
+++ b/src/Symbolic.res
@@ -1,9 +1,9 @@
-module BaseAtom = AtomDef.MakeBaseAtom({
+module Base = AtomBase.Make({
   type t = string
 })
 
 module Atom = {
-  module BaseAtom = BaseAtom
+  module Base = Base
   type t = string
   type subst = Map.t<int, string>
   let unify = (a, b, ~gen as _=?) =>
@@ -27,6 +27,6 @@ module Atom = {
 }
 
 module AtomView = {
-  type props = {name: string, scope: array<string>}
-  let make = (props: props) => React.string(props.name)
+  type props = {atom: string, scope: array<string>}
+  let make = (props: props) => React.string(props.atom)
 }
diff --git a/src/Symbolic.resi b/src/Symbolic.resi
index b865c43..e6a3a25 100644
--- a/src/Symbolic.resi
+++ b/src/Symbolic.resi
@@ -1,3 +1,3 @@
-module BaseAtom: AtomDef.BASE_ATOM with type t = string
-module Atom: AtomDef.ATOM with module BaseAtom = BaseAtom
+module Base: AtomBase.BASE_ATOM with type t = string
+module Atom: AtomDef.ATOM with module Base = Base
 module AtomView: AtomDef.ATOM_VIEW with module Atom := Atom
diff --git a/tests/HOTermTest.res b/tests/HOTermTest.res
index fbd3529..b13f699 100644
--- a/tests/HOTermTest.res
+++ b/tests/HOTermTest.res
@@ -3,13 +3,13 @@ open HOTerm
 
 module Util = TestUtil.MakeTerm(HOTerm)
 
-module Symbol = AtomDef.MakeAtomAndView(
+module Symbol = AtomDef.MakeAtomChoiceAndView(
   Symbolic.Atom,
   Symbolic.AtomView,
-  AtomDef.NilAtomList,
-  AtomDef.NilAtomListView,
+  AtomDef.EmptyAtomChoice,
+  AtomDef.EmptyAtomChoiceView,
 )
-module StringSymbol = AtomDef.MakeAtomAndView(
+module StringSymbol = AtomDef.MakeAtomChoiceAndView(
   StringA.Atom,
   StringA.AtomView,
   Symbol.Atom,
@@ -18,11 +18,11 @@ module StringSymbol = AtomDef.MakeAtomAndView(
 module StringHOTerm = HOTerm.Make(StringSymbol.Atom)
 module StringUtil = TestUtil.MakeTerm(StringHOTerm)
 let wrapString = s => StringHOTerm.Symbol({
-  name: AtomDef.AnyValue(StringA.BaseAtom.Tag, s),
+  name: AtomBase.AnyValue(StringA.Base.Tag, s),
   constructor: false,
 })
 let wrapSymbol = s => StringHOTerm.Symbol({
-  name: AtomDef.AnyValue(Symbolic.BaseAtom.Tag, s),
+  name: AtomBase.AnyValue(Symbolic.Base.Tag, s),
   constructor: false,
 })
 
@@ -169,9 +169,10 @@ zoraBlock("parse and prettyprint", t => {
 })
 
 zoraBlock("string HOTerm functor", t => {
+  module B = AtomBase.String
   t->block("parse string atom", t => {
-    t->StringUtil.testParse(`"x y"`, wrapString([StringA.String("x"), StringA.String("y")]))
-    t->StringUtil.testParse(`"$s"`, ~scope=["s"], wrapString([StringA.Var({idx: 0})]))
+    t->StringUtil.testParse(`"x y"`, wrapString([String("x"), String("y")]))
+    t->StringUtil.testParse(`"$s"`, ~scope=["s"], wrapString([AtomBase.String.Var({idx: 0})]))
     t->StringUtil.testParsePrettyPrint(`"x y"`, `"x y"`)
   })
   t->block("parse symbolic atom", t => {
@@ -179,7 +180,7 @@ zoraBlock("string HOTerm functor", t => {
     t->StringUtil.testParse(
       "@cons",
       StringHOTerm.Symbol({
-        name: AtomDef.AnyValue(Symbolic.BaseAtom.Tag, "cons"),
+        name: AtomBase.AnyValue(Symbolic.Base.Tag, "cons"),
         constructor: true,
       }),
     )
@@ -194,11 +195,11 @@ zoraBlock("string HOTerm functor", t => {
     let substAdd = StringHOTerm.substAdd
     t->equal(
       StringHOTerm.unify(parse(`"a ?0() c"`), parse(`"a b c"`))->Seq.head,
-      Some(emptySubst->substAdd(0, wrapString([StringA.String("b")]))),
+      Some(emptySubst->substAdd(0, wrapString([String("b")]))),
     )
     t->equal(
       StringHOTerm.unify(parse(`(P "?1() a" "?1()")`), parse(`(P "a ?1()" "a")`))->Seq.head,
-      Some(emptySubst->substAdd(1, wrapString([StringA.String("a")]))),
+      Some(emptySubst->substAdd(1, wrapString([String("a")]))),
     )
     let choices =
       StringHOTerm.unify(parse(`"?1() a"`), parse(`"a ?1()"`))
@@ -206,10 +207,7 @@ zoraBlock("string HOTerm functor", t => {
       ->Seq.toArray
     t->equal(
       choices,
-      [
-        emptySubst->substAdd(1, wrapString([])),
-        emptySubst->substAdd(1, wrapString([StringA.String("a")])),
-      ],
+      [emptySubst->substAdd(1, wrapString([])), emptySubst->substAdd(1, wrapString([String("a")]))],
     )
     t->equal(StringHOTerm.unify(parse(`"a"`), parse(`"b"`))->Seq.head, None)
   })
diff --git a/tests/RuleTest.res b/tests/RuleTest.res
index 8ecf8e1..2b9e29b 100644
--- a/tests/RuleTest.res
+++ b/tests/RuleTest.res
@@ -31,13 +31,13 @@ module MakeTest = (Term: TERM, Judgment: JUDGMENT with module Term := Term) => {
   }
 }
 
-module Symbol = AtomDef.MakeAtomAndView(
+module Symbol = AtomDef.MakeAtomChoiceAndView(
   Symbolic.Atom,
   Symbolic.AtomView,
-  AtomDef.NilAtomList,
-  AtomDef.NilAtomListView,
+  AtomDef.EmptyAtomChoice,
+  AtomDef.EmptyAtomChoiceView,
 )
-module StringSymbol = AtomDef.MakeAtomAndView(
+module StringSymbol = AtomDef.MakeAtomChoiceAndView(
   StringA.Atom,
   StringA.AtomView,
   Symbol.Atom,
@@ -45,9 +45,21 @@ module StringSymbol = AtomDef.MakeAtomAndView(
 )
 
 zoraBlock("string terms", t => {
+  module Symbol = AtomDef.MakeAtomChoiceAndView(
+    Symbolic.Atom,
+    Symbolic.AtomView,
+    AtomDef.EmptyAtomChoice,
+    AtomDef.EmptyAtomChoiceView,
+  )
+  module StringSymbol = AtomDef.MakeAtomChoiceAndView(
+    StringA.Atom,
+    StringA.AtomView,
+    Symbol.Atom,
+    Symbol.AtomView,
+  )
   module StringSExp = SExp.Make(StringSymbol.Atom)
-  let wrapString = (s): StringSExp.t => Atom(AtomDef.AnyValue(StringA.BaseAtom.Tag, s))
-  let wrapSymbol = (s): StringSExp.t => Atom(AnyValue(Symbolic.BaseAtom.Tag, s))
+  let wrapString = (s): StringSExp.t => s->AtomBase.String.wrap->Atom
+  let wrapSymbol = (s): StringSExp.t => s->Symbolic.Base.wrap->Atom
   module T = MakeTest(StringSExp, StringSExp)
   t->T.testParseInner(
     `[s1. ("$s1" p) |- ("($s1)" p)]`,
@@ -58,15 +70,12 @@ zoraBlock("string terms", t => {
           vars: [],
           premises: [],
           conclusion: StringSExp.Compound({
-            subexps: [wrapString([StringA.Var({idx: 0})]), wrapSymbol("p")],
+            subexps: [wrapString([Var({idx: 0})]), wrapSymbol("p")],
           }),
         },
       ],
       conclusion: StringSExp.Compound({
-        subexps: [
-          wrapString([StringA.String("("), StringA.Var({idx: 0}), StringA.String(")")]),
-          wrapSymbol("p"),
-        ],
+        subexps: [wrapString([String("("), Var({idx: 0}), String(")")]), wrapSymbol("p")],
       }),
     },
   )
@@ -75,11 +84,11 @@ zoraBlock("string terms", t => {
 zoraBlock("string HOTerms", t => {
   module StringHOTerm = HOTerm.Make(StringSymbol.Atom)
   let wrapString = (s): StringHOTerm.t => Symbol({
-    name: AtomDef.AnyValue(StringA.BaseAtom.Tag, s),
+    name: AtomBase.AnyValue(AtomBase.String.Tag, s),
     constructor: false,
   })
   let wrapSymbol = (s): StringHOTerm.t => Symbol({
-    name: AtomDef.AnyValue(Symbolic.BaseAtom.Tag, s),
+    name: AtomBase.AnyValue(Symbolic.Base.Tag, s),
     constructor: false,
   })
   let app = StringHOTerm.app
@@ -92,13 +101,10 @@ zoraBlock("string HOTerms", t => {
         {
           vars: [],
           premises: [],
-          conclusion: app(wrapString([StringA.Var({idx: 0})]), [wrapSymbol("p")]),
+          conclusion: app(wrapString([Var({idx: 0})]), [wrapSymbol("p")]),
         },
       ],
-      conclusion: app(
-        wrapString([StringA.String("("), StringA.Var({idx: 0}), StringA.String(")")]),
-        [wrapSymbol("p")],
-      ),
+      conclusion: app(wrapString([String("("), Var({idx: 0}), String(")")]), [wrapSymbol("p")]),
     },
   )
 })