diff --git a/index.html b/index.html
index 3b4f2ea..91c1747 100644
--- a/index.html
+++ b/index.html
@@ -248,6 +248,9 @@
   .symbol-nat {
     color: var(--symbol-nat-col)
   }
+  .symbol-prelude {
+    color: var(--symbol-prelude-col)
+  }
   .symbol-turnstile {
       padding-left: 6px;
       padding-right: 6px;
@@ -675,6 +678,38 @@
       (Term (Cons (f nat(2)) (Cons (a nat(0)) Empty)) (Func f (Cons (Const a) (Cons (Var nat(1)) Empty))))
       |- ?
     </hol-string-proof>
+    <hol-string id="index.html/palindrome" deps="index.html/myconfig">
+      a.
+      -------- Eq
+      (Eq a a)
+
+      s.
+      (Eq length("$s") nat(1))
+      ---------------------- Singleton
+      (Singleton "$s")
+
+      s. (Singleton "$s")
+      ---------------------- Rev-1
+      (Rev "$s" "$s")
+
+      s. ss. ssRev. (Rev "$ss" "$ssRev") (Singleton "$s")
+      ----------------------- Rev-n
+      (Rev "$s $ss" "$ssRev $s")
+
+      s. sRev. (Rev "$s" "$sRev")
+      ---------------------- Palindrome-Even
+      (Palindrome "$s $sRev")
+
+      s. sRev. m. (Rev "$s" "$sRev")
+      ---------------------- Palindrome-Odd
+      (Palindrome "$s $m $sRev")
+    </hol-string>
+    <hol-string-proof id="index.html/foobar" deps="index.html/myconfig index.html/palindrome">
+      ------------------ dlads
+      (Palindrome "a b c b a")
+      |- ?
+    </hol-string-proof>
+
     <hol-string id="index.html/string-silliness" deps="index.html/myconfig">
       a.
       -------------- eq-refl
diff --git a/src/AssocComm.res b/src/AssocComm.res
index 10c1240..9cac980 100644
--- a/src/AssocComm.res
+++ b/src/AssocComm.res
@@ -204,6 +204,7 @@ module Make = (
     let full = term->between(token(Const.openTerm), token(Const.closeTerm))
     Parser.runParser(full, str)
   }
+  let reduce = t => t
 
   let substitute = (atom: t, subst: subst): t => {
     let substituted =
diff --git a/src/AtomDef.res b/src/AtomDef.res
index fff14f3..6a84b47 100644
--- a/src/AtomDef.res
+++ b/src/AtomDef.res
@@ -11,6 +11,7 @@ module type ATOM = {
   let upshift: (t, int, ~from: int=?) => t
   let substDeBruijn: (t, array<option<t>>, ~from: int=?) => t
   let concrete: t => bool
+  let reduce: t => t
   let coerce: anyValue => option<t>
 }
 
@@ -45,6 +46,7 @@ module EmptyAtomChoice: ATOM_CHOICE = {
   let upshift = (_, _, ~from as _=?) => throw(AtomExpected)
   let substDeBruijn = (_, _, ~from as _=?) => throw(AtomExpected)
   let concrete = _ => throw(AtomExpected)
+  let reduce = _ => throw(AtomExpected)
 }
 
 module MakeAtomChoice = (Left: ATOM, Right: ATOM_CHOICE): (
@@ -105,6 +107,8 @@ module MakeAtomChoice = (Left: ATOM, Right: ATOM_CHOICE): (
       )->LeftBase.wrap
     )
     ->getOrElse(() => Right.substDeBruijn(atom, substs, ~from?))
+  let reduce = atom =>
+    atom->onLeft(val => Left.reduce(val)->LeftBase.wrap)->getOrElse(() => Right.reduce(atom))
   let concrete = atom => atom->onLeft(Left.concrete)->getOrElse(() => Right.concrete(atom))
 }
 
diff --git a/src/HOTerm.res b/src/HOTerm.res
index 899e102..73ac3eb 100644
--- a/src/HOTerm.res
+++ b/src/HOTerm.res
@@ -36,6 +36,7 @@ module DefaultAtom = {
   let concrete = _ => true
   let upshift = (t, _, ~from as _=?) => t
   let coerce = _ => None
+  let reduce = t => t
 }
 
 module Make = (Atom: AtomDef.ATOM): {
diff --git a/src/Preludic.res b/src/Preludic.res
new file mode 100644
index 0000000..4ce8d8b
--- /dev/null
+++ b/src/Preludic.res
@@ -0,0 +1,108 @@
+module Base = {
+  type t = AtomBase.anyValue
+  type AtomBase.atomTag<_> += Tag: AtomBase.atomTag<t>
+  let wrap = t => t
+  let wrapForReal = t => AtomBase.AnyValue(Tag, t)
+}
+
+type AtomBase.atomTag<_> += LengthTag: AtomBase.atomTag<StringA.t>
+
+exception ShouldNotCallPrelude
+exception NonPreludicValuePassed
+module Atom = {
+  module Base = Base
+  type t = AtomBase.anyValue
+  type subst = Map.t<int, t>
+  // this is probably wrong: we want to unify with any nat
+  let unify = (AtomBase.AnyValue(tagA, a), AtomBase.AnyValue(tagB, b), ~gen=?) => {
+    switch (tagA, tagB) {
+    | (LengthTag, LengthTag) =>
+      StringA.Atom.unify(a, b, ~gen?)->Seq.map(subst =>
+        subst->Util.mapMapValues(s => AtomBase.AnyValue(AtomBase.String.Tag, s))
+      )
+    | _ => Seq.empty
+    }
+  }
+  let prettyPrint = (AtomBase.AnyValue(tag, a), ~scope: array<string>) => {
+    switch tag {
+    | LengthTag => `length(${StringA.Atom.prettyPrint(a, ~scope)})`
+    | _ => throw(NonPreludicValuePassed)
+    }
+  }
+  let parse = (str, ~scope: array<string>, ~gen=?) => {
+    open Parser
+    liftParse(StringA.Atom.parse, ~scope, ~gen?)
+    ->between(token("length("), token(")"))
+    ->map(s => AtomBase.AnyValue(LengthTag, s)->Base.wrapForReal)
+    ->runParser(str)
+  }
+
+  let substitute = (AtomBase.AnyValue(tag, a), subst) => {
+    switch tag {
+    | LengthTag =>
+      AtomBase.AnyValue(
+        LengthTag,
+        a->StringA.Atom.substitute(subst->Util.Map.filterMap((_, v) => StringA.Atom.coerce(v))),
+      )->Base.wrapForReal
+    | _ => throw(NonPreludicValuePassed)
+    }
+  }
+  let substDeBruijn = (AtomBase.AnyValue(tag, a), subst, ~from=?) => {
+    switch tag {
+    | LengthTag => {
+        let subst =
+          a->StringA.Atom.substDeBruijn(
+            subst->Array.map(v => v->Option.flatMap(StringA.Atom.coerce)),
+            ~from?,
+          )
+
+        AtomBase.AnyValue(LengthTag, subst)->Base.wrapForReal
+      }
+    | _ => throw(NonPreludicValuePassed)
+    }
+  }
+
+  let reduce = atom => {
+    let AtomBase.AnyValue(tag, a) = atom
+    switch tag {
+    | LengthTag =>
+      if (
+        a->Array.every(p =>
+          switch p {
+          | AtomBase.String.String(_) => true
+          | _ => false
+          }
+        )
+      ) {
+        AtomBase.AnyValue(AssocCommBase.Nat.Tag, AssocCommBase.Nat.const(Array.length(a)))
+      } else {
+        atom
+      }
+    | _ => throw(NonPreludicValuePassed)
+    }
+  }
+  let concrete = _ => true
+  let upshift = (AtomBase.AnyValue(tag, a), amount, ~from=?) => {
+    switch tag {
+    | LengthTag => AtomBase.AnyValue(LengthTag, a->StringA.Atom.upshift(amount, ~from?))->Base.wrap
+    | _ => throw(NonPreludicValuePassed)
+    }
+  }
+  let coerce = atom => Some(atom)
+}
+
+module AtomView: AtomDef.ATOM_VIEW with module Atom := Atom = {
+  type props = {atom: Atom.t, scope: array<string>}
+  let make = ({atom, scope}) => {
+    let AtomBase.AnyValue(tag, a) = atom
+    switch tag {
+    | LengthTag =>
+      <span>
+        <span className="symbol"> {React.string("length(")} </span>
+        {StringA.AtomView.make({atom: a, scope})}
+        <span className="symbol"> {React.string(")")} </span>
+      </span>
+    | _ => throw(NonPreludicValuePassed)
+    }
+  }
+}
diff --git a/src/SExp.res b/src/SExp.res
index 1d65356..bf23992 100644
--- a/src/SExp.res
+++ b/src/SExp.res
@@ -38,7 +38,12 @@ module Make = (Atom: AtomDef.ATOM): {
   let equivalent = (a: t, b: t) => {
     a == b
   }
-  let reduce = (term: t) => term
+  let rec reduce = (term: t) =>
+    switch term {
+    | Atom(a) => Atom(Atom.reduce(a))
+    | Compound({subexps}) => Compound({subexps: subexps->Array.map(reduce)})
+    | _ => term
+    }
   let rec schematicsIn: t => Belt.Set.t<int, IntCmp.identity> = (it: t) =>
     switch it {
     | Schematic({schematic, _}) => Belt.Set.make(~id=module(IntCmp))->Belt.Set.add(schematic)
diff --git a/src/Scratch.res b/src/Scratch.res
index 05082a4..33d84d2 100644
--- a/src/Scratch.res
+++ b/src/Scratch.res
@@ -60,12 +60,16 @@ module StringNatSymbol = AtomDef.MakeAtomChoiceAndView(
   StringSymbol.Atom,
   StringSymbol.AtomView,
 )
-module StringSExp = SExp.Make(StringNatSymbol.Atom)
-module TermView = SExpView.Make(StringNatSymbol.Atom, StringNatSymbol.AtomView, StringSExp)
-module StringSExpJView = TermViewAsJudgmentView.Make(StringSExp, StringSExp, TermView)
-module AxiomStr = Editable.TextArea(
-  StringAxiomSet.Make(StringNatSymbol.Atom, StringSExp, StringSExpJView),
+module Final = AtomDef.MakeAtomChoiceAndView(
+  Preludic.Atom,
+  Preludic.AtomView,
+  StringNatSymbol.Atom,
+  StringNatSymbol.AtomView,
 )
+module StringSExp = SExp.Make(Final.Atom)
+module TermView = SExpView.Make(Final.Atom, Final.AtomView, StringSExp)
+module StringSExpJView = TermViewAsJudgmentView.Make(StringSExp, StringSExp, TermView)
+module AxiomStr = Editable.TextArea(StringAxiomSet.Make(Final.Atom, StringSExp, StringSExpJView))
 
 module DerivationsOrLemmasStrView = MethodView.CombineMethodView(
   StringSExp,
diff --git a/src/StringA.res b/src/StringA.res
index a0e3f0b..ad44264 100644
--- a/src/StringA.res
+++ b/src/StringA.res
@@ -454,6 +454,7 @@ module Atom = {
 
     acc.contents->Result.map(r => (r, str->String.sliceToEnd(~start=pos.contents)))
   }
+  let reduce = t => t
   let concrete = t =>
     t->Array.every(p =>
       switch p {
@@ -471,6 +472,7 @@ module Atom = {
         | Schematic({schematic, allowed}) => Schematic({schematic, allowed})
         },
       ])
+    | AtomBase.String.Tag => Some(a)
     | AssocCommBase.Nat.Tag => {
         module IntMap = Belt.Map.Int
         if a.schemas->IntMap.size == 0 && a.vars->IntMap.size == 0 {
diff --git a/src/Symbolic.res b/src/Symbolic.res
index cf40c66..db0fe04 100644
--- a/src/Symbolic.res
+++ b/src/Symbolic.res
@@ -23,6 +23,7 @@ module Atom = {
   let substDeBruijn = (name, _, ~from as _=?) => name
   let concrete = _ => true
   let upshift = (t, _, ~from as _=?) => t
+  let reduce = t => t
   let coerce = _ => None
 }
 
diff --git a/tests/PreludeTest.res b/tests/PreludeTest.res
new file mode 100644
index 0000000..f908718
--- /dev/null
+++ b/tests/PreludeTest.res
@@ -0,0 +1,14 @@
+open Zora
+
+module Util = TestUtil.MakeAtomTester(Preludic.Atom)
+module ParseUtil = Util.ParseTester
+
+zoraBlock("parse prelude", t =>
+  t->ParseUtil.testParse(
+    `length("$s")`,
+    ~scope=["s"],
+    Preludic.Base.wrapForReal(
+      AtomBase.AnyValue(Preludic.LengthTag, [AtomBase.String.Var({idx: 0})]),
+    ),
+  )
+)