diff --git a/src/AtomDef.res b/src/AtomDef.res
index 9d29802..eea2257 100644
--- a/src/AtomDef.res
+++ b/src/AtomDef.res
@@ -1,6 +1,6 @@
 // type level stuff to enable well-typed coercions
 type atomTag<_> = ..
-type rec anyValue = HValue(atomTag<'a>, 'a): anyValue
+type rec anyValue = AnyValue(atomTag<'a>, 'a): anyValue
 
 // to allow circular coercions, we declare base types
 // separately from relevant implementation
@@ -17,7 +17,7 @@ module MakeBaseAtom = (
 ): (BASE_ATOM with type t = T.t) => {
   type t = T.t
   type atomTag<_> += Tag: atomTag<t>
-  let wrap = t => HValue(Tag, t)
+  let wrap = t => AnyValue(Tag, t)
 }
 
 module type ATOM = {
@@ -85,7 +85,7 @@ module CombineAtom = (Head: ATOM, Tail: ATOM_LIST): (
   type gen = ref<int>
   let getOrElse = Util.Option.getOrElse
   let coerce = v => Some(v)
-  let onHead = (HValue(tag, val), f: Head.t => 'a): option<'a> =>
+  let onHead = (AnyValue(tag, val), f: Head.t => 'a): option<'a> =>
     switch tag {
     | Head.BaseAtom.Tag => Some(f(val))
     | _ => None
@@ -101,7 +101,7 @@ module CombineAtom = (Head: ATOM, Tail: ATOM_LIST): (
     ->getOrElse(() => Tail.prettyPrint(atom, ~scope))
 
   let unify = (a1, a2, ~gen=?) => {
-    let (HValue(tag1, val1), HValue(tag2, val2)) = (a1, a2)
+    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))
diff --git a/src/SExp.res b/src/SExp.res
index 5fc08ee..3e13c47 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(HValue(AtomDef.SExpTag, AtomDef.Var({idx: idx})))
+    | Var({idx}) => Atom.coerce(AnyValue(AtomDef.SExpTag, AtomDef.Var({idx: idx})))
     | Schematic({schematic, allowed}) =>
-      Atom.coerce(HValue(AtomDef.SExpTag, AtomDef.Schematic({schematic, allowed})))
+      Atom.coerce(AnyValue(AtomDef.SExpTag, AtomDef.Schematic({schematic, allowed})))
     | Compound({subexps: [e1]}) => lower(e1)
     | _ => None
     }
diff --git a/src/Scratch.res b/src/Scratch.res
index 6086d15..c96855d 100644
--- a/src/Scratch.res
+++ b/src/Scratch.res
@@ -57,7 +57,9 @@ module StringSymbol = AtomDef.MakeAtomAndView(
 module StringSExp = SExp.Make(StringSymbol.Atom)
 module TermView = SExpView.Make(StringSymbol.Atom, StringSymbol.AtomView, StringSExp)
 module StringSExpJView = TermViewAsJudgmentView.Make(StringSExp, StringSExp, TermView)
-module AxiomStr = Editable.TextArea(StringAxiomSet)
+module AxiomStr = Editable.TextArea(
+  StringAxiomSet.Make(StringSymbol.Atom, StringSExp, StringSExpJView),
+)
 
 module DerivationsOrLemmasStrView = MethodView.CombineMethodView(
   StringSExp,
diff --git a/src/StringA.res b/src/StringA.res
index c8b6d7c..88d1cfd 100644
--- a/src/StringA.res
+++ b/src/StringA.res
@@ -466,7 +466,7 @@ module Atom = {
       | _ => false
       }
     )
-  let coerce = (AtomDef.HValue(tag, a)) =>
+  let coerce = (AtomDef.AnyValue(tag, a)) =>
     switch tag {
     | Symbolic.BaseAtom.Tag => Some([String(a)])
     | AtomDef.SExpTag =>
diff --git a/src/StringAxiomSet.res b/src/StringAxiomSet.res
index 35905a1..b45b6ef 100644
--- a/src/StringAxiomSet.res
+++ b/src/StringAxiomSet.res
@@ -1,242 +1,222 @@
 open Component
 open! Util
 
-module Symbol = AtomDef.MakeAtomAndView(
-  Symbolic.Atom,
-  Symbolic.AtomView,
-  AtomDef.NilAtomList,
-  AtomDef.NilAtomListView,
-)
-module StringSymbol = AtomDef.MakeAtomAndView(
-  StringA.Atom,
-  StringA.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)
-
-module Rule = Rule.Make(StringSExp, StringSExp)
-module RuleView = RuleView.Make(StringSExp, StringSExp, JudgmentView)
-module Ports = Ports(StringSExp, StringSExp)
-type state = {
-  raw: dict<Rule.t>,
-  derived: dict<Rule.t>,
-}
-
-type props = {
-  content: state,
-  imports: Ports.t,
-  onChange: (state, ~exports: Ports.t=?) => unit,
-}
+module Make = (
+  Atom: AtomDef.ATOM_LIST,
+  Term: module type of SExp.Make(Atom),
+  JudgmentView: Signatures.JUDGMENT_VIEW with module Term := Term and module Judgment := Term,
+) => {
+  module Rule = Rule.Make(Term, Term)
+  module RuleView = RuleView.Make(Term, Term, JudgmentView)
+  module Ports = Ports(Term, Term)
+  type state = {
+    raw: dict<Rule.t>,
+    derived: dict<Rule.t>,
+  }
 
-type judgeGroup = {
-  name: string,
-  rules: array<Rule.t>,
-}
+  type props = {
+    content: state,
+    imports: Ports.t,
+    onChange: (state, ~exports: Ports.t=?) => unit,
+  }
 
-module Set = Belt.Set.String
-let varsInRule = (rule: Rule.t) => {
-  rule.premises->Array.reduce(Set.fromArray(rule.vars), (s, r) =>
-    s->Set.union(Set.fromArray(r.vars))
-  )
-}
+  type judgeGroup = {
+    name: string,
+    rules: array<Rule.t>,
+  }
 
-let getSExpName = (t: StringSExp.t): option<string> =>
-  switch t {
-  | Atom(name) => Some(name->StringSymbol.Atom.prettyPrint(~scope=[]))
-  | _ => None
+  module Set = Belt.Set.String
+  let varsInRule = (rule: Rule.t) => {
+    rule.premises->Array.reduce(Set.fromArray(rule.vars), (s, r) =>
+      s->Set.union(Set.fromArray(r.vars))
+    )
   }
 
-let destructureOpt = (r: StringSExp.t): option<(StringA.Atom.t, string)> =>
-  switch r {
-  | Compound({subexps: [Atom(AtomDef.HValue(tag1, s)), Atom(AtomDef.HValue(tag2, name))]}) =>
-    switch (tag1, tag2) {
-    | (StringA.BaseAtom.Tag, Symbolic.BaseAtom.Tag) => Some((s, name))
+  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))]}) =>
+      switch (tag1, tag2) {
+      | (StringA.BaseAtom.Tag, Symbolic.BaseAtom.Tag) => Some((s, name))
+      | _ => None
+      }
     | _ => 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],
-})
-let findMentionedRuleGroups = (group: judgeGroup, allGroups: array<judgeGroup>): array<
-  judgeGroup,
-> => {
-  let allGroupNames = allGroups->Array.map(g => g.name)
-  let groupNames: array<string> = Array.concat(
-    [group.name],
-    group.rules
-    ->Array.flatMap(r =>
-      r.premises
-      ->Array.filterMap(p => p.conclusion->destructureOpt->Option.map(Pair.second))
-      ->Array.filter(name => allGroupNames->Array.find(name' => name' == name)->Option.isSome)
+  exception InvalidStringInductionPattern
+  let destructure = (r: Term.t): (StringA.Atom.t, string) =>
+    destructureOpt(r)->Option.getOrElse(() => throw(InvalidStringInductionPattern))
+  let structure = (lhs: Term.t, rhs: Term.t): Term.t => Compound({
+    subexps: [lhs, rhs],
+  })
+  let findMentionedRuleGroups = (group: judgeGroup, allGroups: array<judgeGroup>): array<
+    judgeGroup,
+  > => {
+    let allGroupNames = allGroups->Array.map(g => g.name)
+    let groupNames: array<string> = Array.concat(
+      [group.name],
+      group.rules
+      ->Array.flatMap(r =>
+        r.premises
+        ->Array.filterMap(p => p.conclusion->destructureOpt->Option.map(Pair.second))
+        ->Array.filter(name => allGroupNames->Array.find(name' => name' == name)->Option.isSome)
+      )
+      ->Set.fromArray
+      ->Set.remove(group.name)
+      ->Set.toArray,
     )
-    ->Set.fromArray
-    ->Set.remove(group.name)
-    ->Set.toArray,
-  )
-  groupNames->Array.map(name => allGroups->Array.find(g => g.name == name))->Array.keepSome
-}
+    groupNames->Array.map(name => allGroups->Array.find(g => g.name == name))->Array.keepSome
+  }
 
-let derive = (group: judgeGroup, mentionedGroups: array<judgeGroup>): Rule.t => {
-  let allVars =
-    mentionedGroups
-    ->Array.flatMap(g => g.rules)
-    ->Array.reduce(Set.empty, (s, r) => s->Set.union(varsInRule(r)))
-  let rec genVar = (base: string) => {
-    if allVars->Set.has(base) {
-      genVar(`${base}'`)
-    } else {
-      base
+  let derive = (group: judgeGroup, mentionedGroups: array<judgeGroup>): Rule.t => {
+    let allVars =
+      mentionedGroups
+      ->Array.flatMap(g => g.rules)
+      ->Array.reduce(Set.empty, (s, r) => s->Set.union(varsInRule(r)))
+    let rec genVar = (base: string) => {
+      if allVars->Set.has(base) {
+        genVar(`${base}'`)
+      } else {
+        base
+      }
+    }
+    let ps = mentionedGroups->Array.map(g => genVar(`P${g.name}`))
+    let (b, x, a) = (genVar("b"), genVar("x"), genVar("a"))
+    let vars = Array.concat(ps, [b, x, a])
+    let xIdx = vars->Array.findIndex(i => i == x)
+    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})])
+    }
+    let lookupGroup = (name: string): option<int> =>
+      mentionedGroups->Array.findIndexOpt(g => name == g.name)
+    let rec replaceJudgeRHS = (rule: Rule.t, baseIdx: int): Rule.t => {
+      let baseIdx = baseIdx + Array.length(rule.vars)
+      let (s, name) = destructure(rule.conclusion)
+      let inductionHyps =
+        rule.premises
+        ->Array.filter(r =>
+          r.conclusion
+          ->destructureOpt
+          ->Option.flatMap(conclusion => conclusion->Pair.second->lookupGroup)
+          ->Option.isSome
+        )
+        ->Array.map(r => replaceJudgeRHS(r, baseIdx))
+      let pIdx = lookupGroup(name)->Option.getExn
+      {
+        vars: rule.vars,
+        premises: rule.premises->Array.concat(inductionHyps),
+        conclusion: structure(
+          Atom(surround(s, aIdx + baseIdx, bIdx + baseIdx)->StringA.BaseAtom.wrap),
+          Var({idx: pIdx + baseIdx}),
+        ),
+      }
     }
-  }
-  let ps = mentionedGroups->Array.map(g => genVar(`P${g.name}`))
-  let (b, x, a) = (genVar("b"), genVar("x"), genVar("a"))
-  let vars = Array.concat(ps, [b, x, a])
-  let xIdx = vars->Array.findIndex(i => i == x)
-  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})])
-  }
-  let lookupGroup = (name: string): option<int> =>
-    mentionedGroups->Array.findIndexOpt(g => name == g.name)
-  let rec replaceJudgeRHS = (rule: Rule.t, baseIdx: int): Rule.t => {
-    let baseIdx = baseIdx + Array.length(rule.vars)
-    let (s, name) = destructure(rule.conclusion)
-    let inductionHyps =
-      rule.premises
-      ->Array.filter(r =>
-        r.conclusion
-        ->destructureOpt
-        ->Option.flatMap(conclusion => conclusion->Pair.second->lookupGroup)
-        ->Option.isSome
-      )
-      ->Array.map(r => replaceJudgeRHS(r, baseIdx))
-    let pIdx = lookupGroup(name)->Option.getExn
     {
-      vars: rule.vars,
-      premises: rule.premises->Array.concat(inductionHyps),
-      conclusion: structure(
-        Atom(AtomDef.HValue(StringA.BaseAtom.Tag, surround(s, aIdx + baseIdx, bIdx + baseIdx))),
-        Var({idx: pIdx + baseIdx}),
+      vars,
+      premises: Array.concat(
+        [
+          {
+            Rule.vars: [],
+            premises: [],
+            conclusion: structure(Var({idx: xIdx}), Atom(group.name->Symbolic.BaseAtom.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),
+        Var({idx: 0}),
+      ), // TODO: clean here
     }
   }
-  {
-    vars,
-    premises: Array.concat(
-      [
-        {
-          Rule.vars: [],
-          premises: [],
-          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(
-      Atom(HValue(StringA.BaseAtom.Tag, surround([StringA.Var({idx: xIdx})], aIdx, bIdx))),
-      Var({idx: 0}),
-    ), // TODO: clean here
-  }
-}
 
-let deserialise = (str: string, ~imports as _: Ports.t) => {
-  let getBase = (str: string) => {
-    let cur = ref(str)
-    let go = ref(true)
-    let results = Dict.make()
-    let ret = ref(Error("impossible"))
-    while go.contents {
-      switch Rule.parseTopLevel(cur.contents, ~scope=[]) {
-      | Ok((t, n), rest) =>
-        if n->String.trim == "" {
-          go := false
-          ret := Error("Rule given with no name")
-        } else {
-          Dict.set(results, n, t)
-          if rest->String.trim == "" {
+  let deserialise = (str: string, ~imports as _: Ports.t) => {
+    let getBase = (str: string) => {
+      let cur = ref(str)
+      let go = ref(true)
+      let results = Dict.make()
+      let ret = ref(Error("impossible"))
+      while go.contents {
+        switch Rule.parseTopLevel(cur.contents, ~scope=[]) {
+        | Ok((t, n), rest) =>
+          if n->String.trim == "" {
             go := false
-            ret := Ok(results)
+            ret := Error("Rule given with no name")
           } else {
-            cur := rest
+            Dict.set(results, n, t)
+            if rest->String.trim == "" {
+              go := false
+              ret := Ok(results)
+            } else {
+              cur := rest
+            }
+          }
+        | Error(e) => {
+            go := false
+            ret := Error(e)
           }
-        }
-      | Error(e) => {
-          go := false
-          ret := Error(e)
         }
       }
+      ret.contents
     }
-    ret.contents
-  }
-  getBase(str)->Result.map(raw => {
-    let grouped: dict<array<Rule.t>> = Dict.make()
-    raw->Dict.forEach(rule =>
-      switch rule.conclusion->destructureOpt {
-      | Some((_, name)) =>
-        switch grouped->Dict.get(name) {
-        | None => grouped->Dict.set(name, [rule])
-        | Some(rs) => rs->Array.push(rule)
+    getBase(str)->Result.map(raw => {
+      let grouped: dict<array<Rule.t>> = Dict.make()
+      raw->Dict.forEach(rule =>
+        switch rule.conclusion->destructureOpt {
+        | Some((_, name)) =>
+          switch grouped->Dict.get(name) {
+          | None => grouped->Dict.set(name, [rule])
+          | Some(rs) => rs->Array.push(rule)
+          }
+        | _ => ()
         }
-      | _ => ()
-      }
-    )
-    let allGroups = grouped->Dict.toArray->Array.map(((name, rules)) => {name, rules})
-    let derived: Dict.t<Rule.t> = Dict.make()
-    allGroups->Array.forEach(group => {
-      // NOTE: this can clash with other names. is this an issue?
-      derived->Dict.set(`${group.name}_induct`, derive(group, [group]))
-      let mentionedGroups = findMentionedRuleGroups(group, allGroups)
-      if mentionedGroups->Array.length > 1 {
-        derived->Dict.set(`${group.name}_mutualInduct`, derive(group, mentionedGroups))
-      }
+      )
+      let allGroups = grouped->Dict.toArray->Array.map(((name, rules)) => {name, rules})
+      let derived: Dict.t<Rule.t> = Dict.make()
+      allGroups->Array.forEach(group => {
+        // NOTE: this can clash with other names. is this an issue?
+        derived->Dict.set(`${group.name}_induct`, derive(group, [group]))
+        let mentionedGroups = findMentionedRuleGroups(group, allGroups)
+        if mentionedGroups->Array.length > 1 {
+          derived->Dict.set(`${group.name}_mutualInduct`, derive(group, mentionedGroups))
+        }
+      })
+      ({raw, derived}, {Ports.facts: raw->Dict.copy->Dict.assign(derived), ruleStyle: None})
     })
-    ({raw, derived}, {Ports.facts: raw->Dict.copy->Dict.assign(derived), ruleStyle: None})
-  })
-}
+  }
 
-let serialise = (state: state) => {
-  state.raw
-  ->Dict.toArray
-  ->Array.map(((k, r)) => r->Rule.prettyPrintTopLevel(~name=k))
-  ->Array.join("\n")
-}
+  let serialise = (state: state) => {
+    state.raw
+    ->Dict.toArray
+    ->Array.map(((k, r)) => r->Rule.prettyPrintTopLevel(~name=k))
+    ->Array.join("\n")
+  }
 
-let make = props => {
-  let makeRules = content =>
-    <div
-      className={"axiom-set axiom-set-"->String.concat(
-        String.make(props.imports.ruleStyle->Option.getOr(Hybrid)),
-      )}
-    >
-      {content
-      ->Dict.toArray
-      ->Array.mapWithIndex(((n, r), i) =>
-        <RuleView
-          rule={r}
-          scope={[]}
-          key={String.make(i)}
-          style={props.imports.ruleStyle->Option.getOr(Hybrid)}
-        >
-          {React.string(n)}
-        </RuleView>
-      )
-      ->React.array}
+  let make = props => {
+    let makeRules = content =>
+      <div
+        className={"axiom-set axiom-set-"->String.concat(
+          String.make(props.imports.ruleStyle->Option.getOr(Hybrid)),
+        )}
+      >
+        {content
+        ->Dict.toArray
+        ->Array.mapWithIndex(((n, r), i) =>
+          <RuleView
+            rule={r}
+            scope={[]}
+            key={String.make(i)}
+            style={props.imports.ruleStyle->Option.getOr(Hybrid)}
+          >
+            {React.string(n)}
+          </RuleView>
+        )
+        ->React.array}
+      </div>
+    <div>
+      {makeRules(props.content.raw)}
+      <p> {React.string("derived")} </p>
+      {makeRules(props.content.derived)}
     </div>
-  <div>
-    {makeRules(props.content.raw)}
-    <p> {React.string("derived")} </p>
-    {makeRules(props.content.derived)}
-  </div>
+  }
 }
diff --git a/src/Symbolic.res b/src/Symbolic.res
index 8f0474b..f630ebd 100644
--- a/src/Symbolic.res
+++ b/src/Symbolic.res
@@ -24,7 +24,7 @@ module Atom = {
   let concrete = _ => false
   let upshift = (t, _, ~from as _=?) => t
   let coerce = _ => None
-  let wrap = a => AtomDef.HValue(BaseAtom.Tag, a)
+  let wrap = a => AtomDef.AnyValue(BaseAtom.Tag, a)
 }
 
 module AtomView = {
diff --git a/tests/RuleTest.res b/tests/RuleTest.res
index abccc2d..5fb39f6 100644
--- a/tests/RuleTest.res
+++ b/tests/RuleTest.res
@@ -45,8 +45,8 @@ zoraBlock("string terms", t => {
     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))
+  let wrapString = (s): StringSExp.t => Atom(AtomDef.AnyValue(StringA.BaseAtom.Tag, s))
+  let wrapSymbol = (s): StringSExp.t => Atom(AnyValue(Symbolic.BaseAtom.Tag, s))
   module T = MakeTest(StringSExp, StringSExp)
   t->T.testParseInner(
     `[s1. ("$s1" p) |- ("($s1)" p)]`,