diff --git a/src/defck.rs b/src/defck.rs
index 975cb51..4eb0c5e 100644
--- a/src/defck.rs
+++ b/src/defck.rs
@@ -35,8 +35,8 @@ pub struct DefResult {
 impl DefResult {
     /// Returns the definition axiom for the given syntax axiom.
     #[must_use]
-    pub fn definition_for(&self, syntax_axiom: Label) -> Option<&Label> {
-        self.def_map.get(&syntax_axiom)
+    pub fn definition_for(&self, syntax_axiom: Label) -> Option<Label> {
+        self.def_map.get(&syntax_axiom).copied()
     }
 
     /// Returns the list of errors that were generated during the definition check pass.
@@ -54,44 +54,30 @@ impl Database {
     // Parses the 'equality', 'primitive', and 'justification' commmands in the database,
     // and store the result in the database for future fast access.
     fn parse_equality_commands(&self, sset: &SegmentSet, definitions: &mut DefResult) {
+        let nset = self.name_result();
         for sref in sset.segments(..) {
             let buf = &**sref.buffer;
             for (_, (_, command)) in &sref.j_commands {
                 use CommandToken::*;
                 match &**command {
-                    [Keyword(cmd), label, Keyword(from), _reflexivity_law, _commutativity_law, _transitivity_law]
+                    [Keyword(cmd), label, Keyword(from), _reflexivity_law, _symmetry_law, _transitivity_law]
                         if cmd.as_ref(buf) == b"equality" && from.as_ref(buf) == b"from" =>
                     {
-                        let equality = self
-                            .name_result()
-                            .lookup_label(label.value(buf))
-                            .unwrap()
-                            .atom;
+                        let equality = nset.lookup_label(label.value(buf)).unwrap().atom;
+                        // TODO check it's a valid equality
                         definitions.equalities.push(equality);
                     }
-                    [Keyword(cmd), ..] if cmd.as_ref(buf) == b"primitive" => {
-                        for label in &command[1..] {
-                            let primitive = self
-                                .name_result()
-                                .lookup_label(label.value(buf))
-                                .unwrap()
-                                .atom;
+                    [Keyword(cmd), rest @ ..] if cmd.as_ref(buf) == b"primitive" => {
+                        for label in rest {
+                            let primitive = nset.lookup_label(label.value(buf)).unwrap().atom;
                             definitions.primitives.push(primitive);
                         }
                     }
                     [Keyword(cmd), justif_label, Keyword(for_), label]
                         if cmd.as_ref(buf) == b"justification" && for_.as_ref(buf) == b"for" =>
                     {
-                        let theorem = self
-                            .name_result()
-                            .lookup_label(justif_label.value(buf))
-                            .unwrap()
-                            .atom;
-                        let definition = self
-                            .name_result()
-                            .lookup_label(label.value(buf))
-                            .unwrap()
-                            .atom;
+                        let theorem = nset.lookup_label(justif_label.value(buf)).unwrap().atom;
+                        let definition = nset.lookup_label(label.value(buf)).unwrap().atom;
                         definitions.justifications.insert(definition, theorem);
                     }
                     _ => {}
@@ -138,6 +124,8 @@ impl Database {
                 if pending_definitions.len() == 1 {
                     let syntax_axiom = pending_definitions.remove(0);
 
+                    // TODO check that the justification matches the definition
+
                     // Store the validated definition
                     definitions.definitions.insert(definition);
                     definitions.def_map.insert(syntax_axiom, definition);
@@ -154,40 +142,45 @@ impl Database {
                     .stmt_parse_result()
                     .get_formula(&sref)
                     .ok_or_else(|| Diagnostic::UnknownLabel(sref.label_span()))?;
-                let equality = &fmla.get_by_path(&[]).unwrap();
-                if !definitions.equalities.contains(equality) {
+                let root = fmla.root(self);
+                let equality = root.label();
+                if !definitions.equalities.contains(&equality) {
                     Err(Diagnostic::DefCkNotAnEquality(
-                        names.atom_name(*equality).into(),
+                        names.atom_name(equality).into(),
                         definitions
                             .equalities
                             .iter()
-                            .map(|label| names.atom_name(*label).into())
+                            .map(|&label| names.atom_name(label).into())
                             .collect(),
                     ))
                 } else {
+                    let Some(lhs) = root.nth_child(0) else {
+                        return Err(Diagnostic::DefCkMalformedDefinition)
+                    };
+
+                    let syntax_axiom = lhs.label();
+                    // push the definition to the validated list early, so that later definitions
+                    // aren't as messed up if this check fails
+                    definitions.definitions.insert(definition);
+                    if let Some(prev) = definitions.def_map.insert(syntax_axiom, definition) {
+                        return Err(Diagnostic::DefCkDuplicateDefinition(
+                            names.atom_name(syntax_axiom).into(),
+                            names.lookup_label_by_atom(prev).address,
+                        ));
+                    }
+
                     // Remove the definition from the pending list
-                    let syntax_axiom = &fmla.get_by_path(&[0]).unwrap();
-                    let result = if let Some(pending_index) =
-                        pending_definitions.iter().position(|x| *x == *syntax_axiom)
+                    if let Some(pending_index) =
+                        pending_definitions.iter().position(|&x| x == syntax_axiom)
                     {
                         pending_definitions.swap_remove(pending_index);
-                        Ok(())
-                    } else if let Some(previous_saddr) = definitions
-                        .definition_for(*syntax_axiom)
-                        .map(|a| names.lookup_label_by_atom(*a).address)
-                    {
-                        Err(Diagnostic::DefCkDuplicateDefinition(
-                            names.atom_name(*syntax_axiom).into(),
-                            previous_saddr,
-                        ))
                     } else {
-                        Err(Diagnostic::DefCkMalformedDefinition)
-                    };
+                        return Err(Diagnostic::DefCkMalformedDefinition);
+                    }
 
-                    // Store the validated definition
-                    definitions.definitions.insert(definition);
-                    definitions.def_map.insert(*syntax_axiom, definition);
-                    result
+                    // TODO definition check
+
+                    Ok(())
                 }
             }
         }
@@ -198,15 +191,7 @@ impl Database {
         self.parse_equality_commands(sset, definitions);
         let names = self.name_result();
 
-        // Fail the whole check if no equality has been defined
-        #[allow(clippy::manual_assert)]
-        if definitions.equalities.is_empty() {
-            definitions
-                .diagnostics
-                .insert(StatementAddress::default(), Diagnostic::DefCkNoEquality);
-        }
-
-        // TODO verify that the reflexivity, associativity, and transivity laws are well-formed
+        // TODO verify that the reflexivity, symmetry, and transitivity laws are well-formed
 
         let mut pending_definitions = vec![];
         for sref in self
diff --git a/src/formula.rs b/src/formula.rs
index 3f27e27..5c17a69 100644
--- a/src/formula.rs
+++ b/src/formula.rs
@@ -203,6 +203,16 @@ impl Formula {
         FormulaRef { db, formula: self }
     }
 
+    /// Augment a formula with a database reference, to produce a [`FormulaRef`].
+    /// The resulting object implements [`Display`], [`Debug`], and [`IntoIterator`].
+    #[must_use]
+    pub const fn root<'a>(&'a self, db: &'a Database) -> SubFormulaRef<'a> {
+        SubFormulaRef {
+            node_id: self.root,
+            f_ref: self.as_ref(db),
+        }
+    }
+
     /// Debug only, dumps the internal structure of the formula.
     pub fn dump(&self, nset: &Nameset) {
         println!("  Root: {}", self.root);
@@ -223,7 +233,8 @@ impl Formula {
 
     /// Returns the label obtained when following the given path.
     /// Each element of the path gives the index of the child to retrieve.
-    /// For example, the empty
+    /// For example, the empty path gives the root, and the path `[0, 2]`
+    /// in `foo(bar(a, b, baz()), d)` gives `baz`.
     #[must_use]
     pub fn get_by_path(&self, path: &[usize]) -> Option<Label> {
         let mut node_id = self.root;
@@ -462,7 +473,7 @@ impl<'a> Iterator for LabelIter<'a> {
 }
 
 /// A [`Formula`] reference in the context of a [`Database`].
-/// This allows the values in the [`Formula`] to be resolved,
+/// This allows the values in the [`Formula`] to be resolved.
 #[derive(Copy, Clone)]
 pub struct FormulaRef<'a> {
     db: &'a Database,
@@ -478,8 +489,8 @@ impl<'a> std::ops::Deref for FormulaRef<'a> {
 }
 
 impl<'a> FormulaRef<'a> {
-    /// Convert the formula back to a flat list of symbols
-    /// This is slow and shall not normally be called except for showing a result to the user.
+    /// Convert the formula back to a flat list of symbols.
+    /// This is slow and should not normally be called except for showing a result to the user.
     #[must_use]
     pub(crate) fn iter(self) -> Flatten<'a> {
         let mut f = Flatten {
@@ -493,7 +504,7 @@ impl<'a> FormulaRef<'a> {
     }
 
     /// Returns a copy of this formula with a new root
-    /// (in the same tree)
+    /// (in the same tree).
     fn to_rerooted(self, new_root: NodeId) -> Formula {
         Formula {
             root: new_root,
@@ -504,7 +515,7 @@ impl<'a> FormulaRef<'a> {
     }
 
     /// Computes the typecode of the given node
-    /// according to the corresponding statement
+    /// according to the corresponding statement.
     fn compute_typecode_at(&self, node_id: NodeId) -> TypeCode {
         self.db.label_typecode(self.formula.tree[node_id])
     }
@@ -652,7 +663,9 @@ impl<'a> IntoIterator for FormulaRef<'a> {
     }
 }
 
-struct SubFormulaRef<'a> {
+/// A reference to a subformula, usable for tree traversals.
+#[derive(Copy, Clone)]
+pub struct SubFormulaRef<'a> {
     node_id: NodeId,
     f_ref: FormulaRef<'a>,
 }
@@ -679,6 +692,59 @@ impl<'a> Debug for SubFormulaRef<'a> {
     }
 }
 
+impl<'a> SubFormulaRef<'a> {
+    /// Returns the statement label applied at this tree node.
+    #[must_use]
+    pub fn label(&self) -> Label {
+        self.f_ref.formula.tree[self.node_id]
+    }
+
+    /// Returns an iterator over the list of children of this node.
+    pub fn children(&self) -> SubFormulaChildren<'a> {
+        SubFormulaChildren {
+            iter: self.f_ref.formula.tree.children_iter(self.node_id),
+            f_ref: self.f_ref,
+        }
+    }
+
+    /// Returns the `n`th child of this node.
+    #[must_use]
+    pub fn nth_child(&self, index: usize) -> Option<Self> {
+        self.children().nth(index)
+    }
+
+    /// Returns a reference to the subtree obtained when following the given path.
+    /// Each element of the path gives the index of the child to retrieve.
+    /// For example, the empty path gives the root, and the path `[0, 2]`
+    /// in `foo(bar(a, b, baz(c)), d)` gives `baz(c)`.
+    #[must_use]
+    pub fn get_by_path(mut self, path: &[usize]) -> Option<Self> {
+        for &index in path {
+            self = self.nth_child(index)?;
+        }
+        Some(self)
+    }
+}
+
+/// An iterator over the children of a node.
+#[must_use]
+#[derive(Debug)]
+pub struct SubFormulaChildren<'a> {
+    iter: SiblingIter<'a, Label>,
+    f_ref: FormulaRef<'a>,
+}
+
+impl<'a> Iterator for SubFormulaChildren<'a> {
+    type Item = SubFormulaRef<'a>;
+
+    fn next(&mut self) -> Option<Self::Item> {
+        Some(SubFormulaRef {
+            node_id: self.iter.next()?,
+            f_ref: self.f_ref,
+        })
+    }
+}
+
 /// An iterator going through each symbol in a formula
 #[derive(Debug)]
 pub struct Flatten<'a> {