diff --git a/bugs/README.md b/bugs/README.md
new file mode 100644
index 00000000..59517b97
--- /dev/null
+++ b/bugs/README.md
@@ -0,0 +1,96 @@
+# Fixed: induction over computational goals (symbolic-fixpoint reduction)
+
+The three examples here exercise induction over a goal stated with a `Fixpoint`.
+Two of them (`segfault_apply_fixpoint_motive.me`, `segfault_exact_eliminator_fixpoint.me`)
+used to crash the engine with SIGSEGV (exit 139); the third
+(`note_clean_conversion_failure.me`) used to fail cleanly with a type error. **All
+three now run to completion** (exit 0). They are kept as minimal reproducers and
+regression notes.
+
+All involve the same shape: an induction principle whose motive applies a fixpoint
+(`add`) to a *symbolic* recursive argument, so type-checking the step case must
+convert `add (S n) O` to `S (add n O)` with `n` a variable.
+
+Run them with:
+
+```bash
+./build/mengine -q bugs/segfault_apply_fixpoint_motive.me      # exit 0
+./build/mengine -q bugs/segfault_exact_eliminator_fixpoint.me  # exit 0
+./build/mengine -q bugs/note_clean_conversion_failure.me       # exit 0
+```
+
+A complete worked proof of `forall n, add n O = n` by induction now lives in
+`examples/computational_eliminator.me` as permanent regression coverage.
+
+**Follow-on (stdlib-benchmark branch):** the reproducers here use `apply`/`exact`
+of the eliminator with `f_equal`-style step cases.  The standard stdlib idiom —
+`rewrite` on the induction hypothesis, including a *quantified* IH whose type is
+the eliminator's beta-redex `(motive) n` — also works now; see
+`examples/computational_induction_rewrite.me` (`add_succ_r`, `add_comm`) and the
+`Nat` module of `benchmarks/stdlib/`.  The extra fixes that idiom needed are
+listed in `benchmarks/stdlib/README.md` (symbolic-fixpoint reductions stay
+constant-headed; the rewrite path whnf-normalizes a redex-typed IH; the
+eliminator index hole is recorded during `fill_hole`).
+
+## Root cause
+
+The shared root cause was non-termination when a fixpoint is unfolded on a
+*symbolic* (variable) recursive argument. Three issues conspired:
+
+1. **Unconditional fix reduction.** `conversion_whnf` / `normalize_whnf` / `cbv`
+   reduced a fixpoint application regardless of its decreasing argument. With `n`
+   a variable, `add n O` unfolded to `match n with O => O | S p => S (add p O)`;
+   `conversion_derivable` then recursed into the `S` branch (`add p O`), which
+   unfolded again, forever — a stack overflow / SIGSEGV in the eliminator paths.
+
+2. **A fixpoint constant was delta-reducible to its eta-expanded lambda form.**
+   `Fixpoint add …` registered the recursive variable's body as
+   `λn. λm. body`, so `add` unfolded unconditionally via delta+beta and a fix
+   node never actually appeared during reduction — the guard in (3) had nothing to
+   bite on.
+
+3. **`fix_reduce` captured shared binders.** It substituted the fix node inline
+   for the recursive variable, but the fix shares its argument binders with the
+   body, so re-wrapping them in lambdas double-bound those variables.
+
+## The fix
+
+- `src/kernel/fix_reduction.c` adds `fix_reduce_app`, the guarded fix rule: an
+  application whose head is a fix reduces only once its decreasing argument is in
+  constructor head normal form. `conversion_whnf`, `normalize_whnf`, and `cbv`
+  call it instead of reducing fixpoints unconditionally; a bare fix is now a
+  value. So `add n O` (symbolic `n`) stays stuck and conversion compares it
+  structurally — terminating.
+
+- `src/kernel/expression.c` registers the **fix node itself** as the recursive
+  variable's definitional body (not the eta-expanded lambda). Unfolding the
+  constant now yields a fix node, so the guard governs it. Recursive calls inside
+  the body resolve through the recursive variable (via delta), so `fix_reduce`
+  no longer substitutes inline — it just strips the fix to its lambda abstraction,
+  avoiding the binder capture in (3).
+
+- `src/commandlanguage/command_exec.c` makes the `Definition` command accept a
+  declared type that is *convertible* (not merely structurally congruent) to the
+  inferred type, so computational types such as `add O O = O` are accepted.
+
+All 431 kernel tests and every `examples/*.me` still pass.
+
+## Previously fixed on this branch (related, but distinct)
+
+Two adjacent crashes/limitations were fixed earlier to unblock the Rocq-stdlib
+benchmark (`benchmarks/stdlib/`); they are independent of the symbolic-fixpoint
+crash above:
+
+1. **`cbv` did not reduce applied fixpoints.** `_normalize_cbv` only tried beta
+   on an application spine, so `cbv`/`Eval` left `add (S O) O` stuck even though
+   the conversion checker could reduce it. `src/kernel/normalize.c` now unfolds
+   `(fix …) arg` in the APP case, mirroring `normalize_whnf`.
+
+2. **GC double-free on *ground* computational eliminators.** Type-checking a
+   fully ground eliminator whose motive needs reduction (e.g. `destruct b` on
+   `negb (negb b) = b`) produced a correct proof term but crashed at shutdown:
+   `MatchBranch` arrays are shared by pointer across arena nodes (normalize/
+   conversion rebuild a match with a new scrutinee but reuse its branches), and
+   `expression_gc_shutdown` freed them per-node. It now frees each shared
+   allocation exactly once (`src/kernel/expression.c`). This is shutdown-only
+   memory hygiene and cannot affect proof soundness.
diff --git a/bugs/note_clean_conversion_failure.me b/bugs/note_clean_conversion_failure.me
new file mode 100644
index 00000000..07ac309e
--- /dev/null
+++ b/bugs/note_clean_conversion_failure.me
@@ -0,0 +1,17 @@
+(* FIXED (now exit 0). This used to fail cleanly (exit 1) with a type error.
+
+   It showed the underlying limitation behind the two segfaults: a Fixpoint applied
+   to a constructor-headed *symbolic* argument, `add (S n) O`, must reduce to
+   `S (add n O)` with `n` a variable. The `Definition` command also now accepts a
+   declared type convertible (not merely structurally congruent) to the inferred
+   one, so this is checked by reduction; see bugs/README.md.
+
+   Run: ./build/mengine -q bugs/note_clean_conversion_failure.me *)
+
+Inductive nat : Type := | O : nat | S : forall (_: nat), nat.
+
+Fixpoint add (n : nat) (m : nat) {struct n} : nat :=
+  match n with | O => m | S p => S (add p m) end.
+
+Definition step_conv : forall (n : nat), eq nat (add (S n) O) (S (add n O)) :=
+  fun (n : nat) => eq_refl nat (S (add n O)).
diff --git a/bugs/note_dangling_options_pointer.md b/bugs/note_dangling_options_pointer.md
new file mode 100644
index 00000000..4e7309da
--- /dev/null
+++ b/bugs/note_dangling_options_pointer.md
@@ -0,0 +1,90 @@
+# Fixed: dangling `MEngineOptions *` (use-after-return under ASan)
+
+**Status:** **fixed** — `mengine_runtime_new` now owns a private copy of the
+options (`src/runtime/runtime.c`).  Discovered while validating the
+parametric-list kernel fixes under AddressSanitizer; pre-existing and unrelated to
+those fixes.  Kept as a note because the symptom is subtle (benign without ASan)
+and the by-reference API was a footgun.
+
+## Symptom
+
+`make check` built with AddressSanitizer aborts partway through the integration
+suite:
+
+```
+==…==ERROR: AddressSanitizer: stack-use-after-return on address 0x…
+    #0 debug_print_token        src/common/lexer.c:48
+    #1 lexer_next_token         src/common/lexer.c:254
+    #2 parser_init              src/common/parser_base.c:12
+    #3 mengine_runtime_exec_string  src/runtime/runtime.c:127
+    #4 run_ok                   tests/engine/test_integration.c:14
+    #5 test_axiom_and_check     tests/engine/test_integration.c:30
+  …
+  #0 …                          tests/engine/test_integration.c:5   (the freed frame)
+```
+
+Reproduce (no clang needed — gcc has ASan too):
+
+```bash
+make clean
+make CC=gcc CFLAGS="-Wall -Wextra -O0 -g -I. -fsanitize=address -fno-omit-frame-pointer" \
+         LDFLAGS="-fsanitize=address" check
+```
+
+The **default (non-ASan) build is unaffected** — all 431 tests pass — because the
+freed stack slot still happens to hold the old option bytes, so the reads return
+plausible values.  It is a genuine use-after-return, just a normally-benign one.
+
+## Root cause
+
+`mengine_runtime_new` **borrows** its options by pointer rather than copying them:
+
+```c
+// src/runtime/runtime.c
+MEngineRuntime *mengine_runtime_new(MEngineOptions *options) {
+    …
+    rt->options = options;   // stores the caller's pointer, no copy
+    …
+}
+```
+
+The runtime then keeps reading through that pointer for the rest of its life
+(`runtime.c:124` `lexer_init(&lx, source, rt->options)` → `lexer_next_token` →
+`debug_print_token`, which dereferences `lx->options->debug` at `lexer.c:48`).
+
+The integration-test helper hands it a pointer to a **stack local** and then
+returns:
+
+```c
+// tests/engine/test_integration.c
+static MEngineRuntime *make_rt(void) {
+    MEngineOptions opts = {0};        // lives only in this frame
+    opts.quiet = true;
+    return mengine_runtime_new(&opts);  // runtime keeps &opts after make_rt returns
+}
+```
+
+When `make_rt` returns, `opts` is gone, but `rt->options` still points at that
+reclaimed frame.  The next lex/parse dereferences it → stack-use-after-return.
+
+`src/main.c` avoids the trap only by luck of lifetime: its options struct lives in
+`main`'s frame, which outlives the runtime, so the borrowed pointer never dangles.
+
+## The fix
+
+Option 1 (own the options) was taken: `mengine_runtime_new` allocates
+`rt->options = malloc(sizeof(MEngineOptions))` and copies the caller's struct into
+it (`*rt->options = *options`), and `mengine_runtime_free` frees it.  This removes
+the lifetime footgun for every caller — the runtime no longer depends on the
+caller keeping the options struct alive.  The transient mutations through
+`rt->options` (the `quiet` toggle while loading the prelude, `execution_type`)
+were already internal to the runtime, so copying does not change observable
+behaviour; `main.c` passes options by value and never reads them back.
+
+The alternative (give the test's options a lifetime ≥ the runtime) was rejected as
+narrower — it would have left the by-reference API as a trap for the next caller.
+
+Verified: `make check` built with AddressSanitizer now runs to completion (431/431,
+no `stack-use-after-return`).  No `.me` reproducer — this is a C-level lifetime bug
+in the runtime, not a kernel or proof-checking bug, and it cannot affect proof
+soundness.
diff --git a/bugs/segfault_apply_fixpoint_motive.me b/bugs/segfault_apply_fixpoint_motive.me
new file mode 100644
index 00000000..2a6f853d
--- /dev/null
+++ b/bugs/segfault_apply_fixpoint_motive.me
@@ -0,0 +1,18 @@
+(* FIXED (now exit 0). This used to SIGSEGV (exit 139).
+
+   Applying an induction principle whose motive mentions a Fixpoint crashed the
+   `apply` tactic while it unified the principle with the goal and built the
+   subgoals — the natural route an induction proof of `add n O = n` takes. The
+   guarded fix rule (src/kernel/fix_reduction.c) now keeps the conversion
+   terminating; see bugs/README.md.
+
+   Run: ./build/mengine -q bugs/segfault_apply_fixpoint_motive.me *)
+
+Inductive nat : Type := | O : nat | S : forall (_: nat), nat.
+
+Fixpoint add (n : nat) (m : nat) {struct n} : nat :=
+  match n with | O => m | S p => S (add p m) end.
+
+Theorem add_O_r : forall (n : nat), eq nat (add n O) n.
+intro n.
+apply (nat_ind (fun (k : nat) => eq nat (add k O) k)).
diff --git a/bugs/segfault_exact_eliminator_fixpoint.me b/bugs/segfault_exact_eliminator_fixpoint.me
new file mode 100644
index 00000000..533035f1
--- /dev/null
+++ b/bugs/segfault_exact_eliminator_fixpoint.me
@@ -0,0 +1,20 @@
+(* FIXED (now exit 0). This used to SIGSEGV (exit 139).
+
+   Type-checking a fully explicit eliminator proof term crashed in the step case,
+   where `add (S n) O` must convert to `S (add n O)` under the `n` binder. Fix
+   reduction is now guarded on the decreasing argument being constructor-headed,
+   so `add n O` (symbolic `n`) stays stuck instead of unfolding forever; see
+   bugs/README.md.
+
+   Run: ./build/mengine -q bugs/segfault_exact_eliminator_fixpoint.me *)
+
+Inductive nat : Type := | O : nat | S : forall (_: nat), nat.
+
+Fixpoint add (n : nat) (m : nat) {struct n} : nat :=
+  match n with | O => m | S p => S (add p m) end.
+
+Axiom f_equal_S : forall (a : nat), forall (b : nat), forall (_: eq nat a b),
+  eq nat (S a) (S b).
+
+Check (nat_ind (fun (k : nat) => eq nat (add k O) k) (eq_refl nat O)
+        (fun (n : nat) => fun (ih : eq nat (add n O) n) => f_equal_S (add n O) n ih)).
diff --git a/examples/computational_eliminator.me b/examples/computational_eliminator.me
new file mode 100644
index 00000000..8c491a96
--- /dev/null
+++ b/examples/computational_eliminator.me
@@ -0,0 +1,54 @@
+(* computational_eliminator.me
+
+   Regression coverage for two kernel fixes made for the Rocq-stdlib benchmark
+   (benchmarks/stdlib/).  Both must hold for this file to run to completion:
+
+   1. `cbv` reduces an *applied* fixpoint/definition.  Before the fix
+      `_normalize_cbv` only tried beta on an application spine, so `cbv` left
+      `negb (negb true)` and `add (S O) O` stuck.  Here each case below is closed
+      by `cbv` followed by the (syntactic) prelude `reflexivity`, which only
+      matches once `cbv` has reduced both sides to the same normal form.
+
+   2. Type-checking a *ground* computational eliminator no longer crashes.
+      `apply (bool_ind motive)` on a goal whose motive applies `negb` used to
+      build a correct proof term but then double-free / SIGSEGV at GC shutdown
+      (shared MatchBranch arrays).  If that regressed, this file would exit 139. *)
+
+Inductive bool : Type := | true : bool | false : bool.
+
+Definition negb : forall (_ : bool), bool :=
+  fun (b : bool) => match b with | true => false | false => true end.
+
+(* Ground computational case analysis via the generated eliminator. *)
+Theorem negb_involutive : forall (b : bool), eq bool (negb (negb b)) b.
+intro b.
+apply (bool_ind (fun (b : bool) => eq bool (negb (negb b)) b)).
+cbv. reflexivity.
+cbv. reflexivity.
+
+Inductive nat : Type := | O : nat | S : forall (n : nat), nat.
+
+Fixpoint add (n : nat) (m : nat) {struct n} : nat :=
+  match n with | O => m | S p => S (add p m) end.
+
+(* cbv must reduce the applied fixpoint for these to print their normal forms. *)
+Eval cbv in (add (S O) O).
+Eval cbv in (add (S (S O)) (S (S O))).
+
+(* Induction over a goal stated with a Fixpoint applied to a *symbolic* recursive
+   argument.  Proving this by `nat_ind` used to SIGSEGV (exit 139): type-checking the
+   step case converts `add (S p) O` with `p` a variable, and fix reduction was
+   unconditional, so a fixpoint unfolded forever on its non-constructor recursive
+   argument.  Reduction now fires only once the decreasing argument is
+   constructor-headed (see src/kernel/fix_reduction.c), so `add p O` stays stuck and
+   the conversion terminates.  If that regresses, this proof crashes or fails. *)
+Axiom f_equal_S : forall (a : nat), forall (b : nat), forall (_ : eq nat a b),
+  eq nat (S a) (S b).
+
+Theorem add_O_r : forall (n : nat), eq nat (add n O) n.
+intro n.
+apply (nat_ind (fun (k : nat) => eq nat (add k O) k)).
+cbv. reflexivity.
+intro p.
+intro ih.
+cbv. apply f_equal_S. exact ih.
diff --git a/examples/computational_induction_rewrite.me b/examples/computational_induction_rewrite.me
new file mode 100644
index 00000000..b14c6e46
--- /dev/null
+++ b/examples/computational_induction_rewrite.me
@@ -0,0 +1,58 @@
+(* computational_induction_rewrite.me
+
+   Regression coverage for computational induction proved with `rewrite` on a
+   *quantified* induction hypothesis — the idiom the Rocq standard library uses
+   for arithmetic.  Exercises four fixes that must all hold together:
+
+   1. fix_reduction.c / normalize.c: a fixpoint constant stays folded (and so
+      `rewrite`-matchable) when its decreasing argument is symbolic, and fires
+      via fix_reduce_app once it is constructor-headed.  So `simpl` turns
+      `add (S n) m` into `S (add n m)` while leaving the stuck `add n m` headed
+      by the `add` constant rather than a bare fix node.
+   2. unify.c / rewrite_internal.c: `rewrite` reads the equation off an IH whose
+      stored type is the eliminator's beta-redex `(motive) n` by weak-head
+      normalizing it first, and instantiates the IH's `forall`.
+   3. expression.c: such a redex-typed IH can be *applied* (the syntactic-Pi
+      precheck in init_app_expression_wc was removed; _construct_app_type whnfs).
+   4. type_compat.c: the eliminator's index hole (left by a quantified motive) is
+      recorded during fill, instead of lingering as a stray open goal. *)
+
+Inductive nat : Type := | O : nat | S : forall (n : nat), nat.
+
+Fixpoint add (n : nat) (m : nat) {struct n} : nat :=
+  match n with | O => m | S p => S (add p m) end.
+
+(* simpl/reflexivity/symmetry as the stdlib compat prelude defines them: simpl is
+   full cbv, and reflexivity closes by conversion (so `add O (S m)` and `S m` need
+   not be syntactically equal, only convertible). *)
+Tactic simpl := cbv.
+Tactic reflexivity := match Goal with
+| [ |- (((eq ?A) ?x) ?y) ] => exact ((eq_refl A) x)
+end.
+Tactic symmetry := apply eq_sym.
+
+(* add_succ_r: the IH `IHn : forall m, add n (S m) = S (add n m)` is quantified,
+   and its type is the eliminator's redex `(motive) n`.  `rewrite IHn with eq`
+   must whnf that type, instantiate `m`, and rewrite the stuck `add n (S m)`. *)
+Theorem add_succ_r : forall (n : nat), forall (m : nat),
+  eq nat (add n (S m)) (S (add n m)).
+intro n.
+apply (nat_ind (fun (n : nat) => forall (m : nat),
+  eq nat (add n (S m)) (S (add n m)))).
+simpl. intro m. reflexivity.
+intro n. intro IHn. simpl. intro m. simpl. rewrite IHn with eq. reflexivity.
+
+Theorem add_0_r : forall (n : nat), eq nat (add n O) n.
+intro n.
+apply (nat_ind (fun (n : nat) => eq nat (add n O) n)).
+simpl. reflexivity.
+intro n. intro IHn. simpl. rewrite IHn with eq. reflexivity.
+
+(* add_comm builds on add_succ_r and add_0_r, mixing rewrite/symmetry the way a
+   real stdlib proof does. *)
+Theorem add_comm : forall (n : nat), forall (m : nat), eq nat (add n m) (add m n).
+intro n.
+apply (nat_ind (fun (n : nat) => forall (m : nat), eq nat (add n m) (add m n))).
+simpl. intro m. simpl. symmetry. rewrite add_0_r with eq. reflexivity.
+intro n. intro IHn. simpl. intro m. simpl. rewrite IHn with eq. symmetry.
+rewrite add_succ_r with eq. reflexivity.
diff --git a/src/commandlanguage/command_exec.c b/src/commandlanguage/command_exec.c
index edbb9ed8..b8f05cf4 100644
--- a/src/commandlanguage/command_exec.c
+++ b/src/commandlanguage/command_exec.c
@@ -98,7 +98,21 @@ static int _handle_definition_command(MEngineRuntime *rt, DefinitionCmd *defn_cm
         fprintf(stderr, ERROR "Error:" CRESET " definition '%s' has a invalid type.\n", name);
     }
 
-    if (!kernel_expr_congruent(inferred_type_def_body, expected_type_def_body)) {
+    // Accept the definition when the inferred and declared types are convertible,
+    // not merely structurally congruent. The fast structural check avoids the cost of
+    // full conversion in the common case; the fallback lets computational types match
+    // (e.g. a declared `add O O` against an inferred `O`).
+    bool types_match = kernel_expr_congruent(inferred_type_def_body, expected_type_def_body);
+    if (!types_match) {
+        Conversion *conv = kernel_expr_conversion_in_context(
+            rendered_type_ctx, inferred_type_def_body, expected_type_def_body);
+        if (conv) {
+            types_match = true;
+            kernel_conversion_free(conv);
+        }
+    }
+
+    if (!types_match) {
         fprintf(stderr, ERROR "Type error:" CRESET " definition '%s' has a mismatched type.\n",
                 name);
         char *_s1 = kernel_expr_to_string(expected_type_def_body);
@@ -260,8 +274,8 @@ static int _handle_print_command(MEngineRuntime *rt, PrintCmd *print_cmd) {
     return 0;
 }
 
-static Expression *_build_constructor_case_type(Expression *ctor_expr, Expression *ctor_type,
-                                                Expression *motive_var, Expression **param_vars,
+static Expression *_build_constructor_case_type(Expression *ctor_expr, Expression *motive_var,
+                                                Expression *ind_var, Expression **param_vars,
                                                 size_t param_count, size_t index_count,
                                                 Context *elim_ctx);
 
@@ -341,10 +355,23 @@ static Expression *_build_induction_principle_type(InductiveCmd *ind_cmd, Expres
                                                    Context **contexts) {
     Context *elim_ctx = contexts[param_count];
 
+    // The inductive's own parameter variables (param_vars) were built in a context
+    // branch created *before* ind_var, so they are not in scope where the principle
+    // lives. Re-bind one shared set of parameters here, after ind_var; the motive,
+    // every constructor case, and the conclusion all refer to these. Parameter
+    // types are taken verbatim, which assumes a parameter's type does not mention
+    // earlier parameters (the usual case, e.g. `(A : Type)`).
+    Expression **params = malloc(param_count * sizeof(Expression *));
+    for (size_t i = 0; i < param_count; i++) {
+        params[i] = kernel_var_create(kernel_var_name(param_vars[i]),
+                                      kernel_expr_type(param_vars[i]), elim_ctx);
+        elim_ctx = params[i];
+    }
+
     Expression **index_vars = NULL;
     size_t index_count = 0;
     Expression *motive_type =
-        _build_motive_type(ind_var, param_vars, param_count, elim_ctx, &index_vars, &index_count);
+        _build_motive_type(ind_var, params, param_count, elim_ctx, &index_vars, &index_count);
     Expression *motive_var = kernel_var_create("P", motive_type, elim_ctx);
     elim_ctx = motive_var;
 
@@ -358,18 +385,19 @@ static Expression *_build_induction_principle_type(InductiveCmd *ind_cmd, Expres
         Expression *ctor_expr = kernel_context_lookup(elim_ctx, ctor->name);
         if (!ctor_expr) {
             fprintf(stderr, ERROR "Constructor %s not found in context\n" CRESET, ctor->name);
+            free(params);
             free(case_vars);
             free(case_contexts);
             return NULL;
         }
 
-        Expression *ctor_type = kernel_expr_type(ctor_expr);
         Expression *case_type =
-            _build_constructor_case_type(ctor_expr, ctor_type, motive_var, param_vars, param_count,
+            _build_constructor_case_type(ctor_expr, motive_var, ind_var, params, param_count,
                                          index_count, case_contexts[i]);
 
         if (!case_type) {
             fprintf(stderr, ERROR "Failed to build case type for %s\n" CRESET, ctor->name);
+            free(params);
             free(case_vars);
             free(case_contexts);
             return NULL;
@@ -380,6 +408,7 @@ static Expression *_build_induction_principle_type(InductiveCmd *ind_cmd, Expres
         case_vars[i] = kernel_var_create(case_name, case_type, case_contexts[i]);
         if (!case_vars[i]) {
             fprintf(stderr, ERROR "Failed to create case variable for %s\n" CRESET, ctor->name);
+            free(params);
             free(case_vars);
             free(case_contexts);
             return NULL;
@@ -407,13 +436,14 @@ static Expression *_build_induction_principle_type(InductiveCmd *ind_cmd, Expres
     // Build (ind params concl_index_0 ... concl_index_n)
     Expression *ind_applied = ind_var;
     for (size_t i = 0; i < param_count; i++) {
-        ind_applied = kernel_app_create(ind_applied, param_vars[i], final_ctx);
+        ind_applied = kernel_app_create(ind_applied, params[i], final_ctx);
         if (!ind_applied) {
             fprintf(stderr,
                     ERROR
                     "Failed to apply parameter %zu to inductive in "
                     "conclusion\n" CRESET,
                     i);
+            free(params);
             free(case_vars);
             free(case_contexts);
             if (index_vars) {
@@ -441,6 +471,7 @@ static Expression *_build_induction_principle_type(InductiveCmd *ind_cmd, Expres
     target_applied = kernel_app_create(target_applied, target_var, target_ctx);
     if (!target_applied) {
         fprintf(stderr, ERROR "Failed to apply motive to target\n" CRESET);
+        free(params);
         free(case_vars);
         free(case_contexts);
         if (index_vars) {
@@ -468,6 +499,7 @@ static Expression *_build_induction_principle_type(InductiveCmd *ind_cmd, Expres
         result = kernel_forall_create(case_vars[i - 1], result);
         if (!result) {
             fprintf(stderr, ERROR "Failed to wrap with constructor case %zu\n" CRESET, i - 1);
+            free(params);
             free(case_vars);
             free(case_contexts);
             return NULL;
@@ -477,21 +509,24 @@ static Expression *_build_induction_principle_type(InductiveCmd *ind_cmd, Expres
     result = kernel_forall_create(motive_var, result);
     if (!result) {
         fprintf(stderr, ERROR "Failed to wrap with motive P\n" CRESET);
+        free(params);
         free(case_vars);
         free(case_contexts);
         return NULL;
     }
 
     for (size_t i = param_count; i > 0; i--) {
-        result = kernel_forall_create(param_vars[i - 1], result);
+        result = kernel_forall_create(params[i - 1], result);
         if (!result) {
             fprintf(stderr, ERROR "Failed to wrap with parameter %zu\n" CRESET, i - 1);
+            free(params);
             free(case_vars);
             free(case_contexts);
             return NULL;
         }
     }
 
+    free(params);
     free(case_vars);
     free(case_contexts);
     if (index_vars) {
@@ -500,127 +535,147 @@ static Expression *_build_induction_principle_type(InductiveCmd *ind_cmd, Expres
     return result;
 }
 
-static Expression *_build_constructor_case_type(Expression *ctor_expr, Expression *ctor_type,
-                                                Expression *motive_var, Expression **param_vars,
-                                                size_t param_count, size_t index_count,
-                                                Context *elim_ctx) {
-    Expression *core_type = ctor_type;
-    for (size_t i = 0; i < param_count; i++) {
-        if (kernel_forall_var(core_type) != NULL) {
-            core_type = kernel_forall_body(core_type);
-        }
+// Build the induction hypothesis for a single constructor argument, or NULL when
+// the argument is not a recursive occurrence of the inductive being defined.
+//
+// An argument `arg : I p0..p_{m-1} x0..x_{k-1}` (the inductive applied to its
+// parameters and indices) yields the hypothesis `P x0..x_{k-1} arg` — the motive
+// applied to the argument's own indices and then the argument itself. This is
+// what turns the generated principle from plain case analysis into induction.
+//
+// Only first-order recursion is recognised; a higher-order argument such as
+// `(nat -> I)` is treated as non-recursive and gets no hypothesis.
+static Expression *_build_recursive_arg_hypothesis(Expression *arg_var, Expression *arg_type,
+                                                   Expression *ind_var, Expression *motive_var,
+                                                   size_t param_count, size_t index_count,
+                                                   Context *ctx) {
+    if (!kernel_expr_congruent(kernel_expr_head(arg_type), ind_var)) {
+        return NULL;
     }
 
-    DoublyLinkedList *arg_types = dll_create();
-    Expression *current = core_type;
-    while (kernel_forall_var(current) != NULL) {
-        Expression *arg_type = kernel_expr_type(kernel_forall_var(current));
-        dll_insert_at_tail(arg_types, dll_new_node(arg_type));
-        current = kernel_forall_body(current);
+    Expression *hypothesis = motive_var;
+    if (index_count > 0) {
+        // arg_type is the spine `I p0..p_{m-1} x0..x_{k-1}`; the indices are the
+        // arguments past the parameters.
+        DoublyLinkedList *spine = dll_create();
+        Expression *head = arg_type;
+        while (kernel_app_func(head) != NULL) {
+            dll_insert_at_head(spine, dll_new_node(kernel_app_arg(head)));
+            head = kernel_app_func(head);
+        }
+        for (size_t i = 0; i < index_count; i++) {
+            Expression *index = (Expression *)dll_at(spine, param_count + i)->data;
+            hypothesis = kernel_app_create(hypothesis, index, ctx);
+        }
+        dll_destroy(spine);
     }
+    return kernel_app_create(hypothesis, arg_var, ctx);
+}
 
+static Expression *_build_constructor_case_type(Expression *ctor_expr, Expression *motive_var,
+                                                Expression *ind_var, Expression **param_vars,
+                                                size_t param_count, size_t index_count,
+                                                Context *elim_ctx) {
+    // Instantiate the constructor at the principle's parameters by applying it,
+    // rather than stripping parameter binders from its type textually. The kernel
+    // substitutes the parameters into the resulting argument and return types, so
+    // everything below is expressed in terms of param_vars and valid in elim_ctx.
     Expression *ctor_app = ctor_expr;
     for (size_t i = 0; i < param_count; i++) {
         ctor_app = kernel_app_create(ctor_app, param_vars[i], elim_ctx);
         if (!ctor_app) {
             fprintf(stderr, ERROR "Failed to apply parameter %zu to constructor\n" CRESET, i);
-            dll_destroy(arg_types);
             return NULL;
         }
     }
 
-    size_t arg_count = dll_len(arg_types);
-    Expression **arg_vars = malloc(arg_count * sizeof(Expression *));
+    // Walk the parameter-instantiated constructor telescope, creating a fresh
+    // variable for each argument. After applying each fresh argument we recompute
+    // the remaining type from the partial application, so the kernel rebases the
+    // following argument and return types onto our fresh variables — keeping them
+    // valid here even when a type mentions an earlier argument or a parameter
+    // (e.g. cons's tail of type `list A`).
+    DoublyLinkedList *args = dll_create();
+    Expression *current = kernel_expr_type(ctor_app);
     Context *case_ctx = elim_ctx;
-
-    for (size_t i = 0; i < arg_count; i++) {
-        Expression *arg_type = (Expression *)dll_at(arg_types, i)->data;
+    size_t arg_i = 0;
+    while (kernel_forall_var(current) != NULL) {
+        Expression *arg_type = kernel_expr_type(kernel_forall_var(current));
         char arg_name[32];
-        sprintf(arg_name, "arg%zu", i);
-
-        arg_vars[i] = kernel_var_create(arg_name, arg_type, case_ctx);
-        case_ctx = arg_vars[i];
-        ctor_app = kernel_app_create(ctor_app, arg_vars[i], case_ctx);
+        sprintf(arg_name, "arg%zu", arg_i++);
+        Expression *arg_var = kernel_var_create(arg_name, arg_type, case_ctx);
+        dll_insert_at_tail(args, dll_new_node(arg_var));
+        case_ctx = arg_var;
+        ctor_app = kernel_app_create(ctor_app, arg_var, case_ctx);
         if (!ctor_app) {
-            fprintf(stderr, ERROR "Failed to apply constructor arg %zu\n" CRESET, i);
-            dll_destroy(arg_types);
-            free(arg_vars);
+            fprintf(stderr, ERROR "Failed to apply constructor argument\n" CRESET);
+            dll_destroy(args);
             return NULL;
         }
+        current = kernel_expr_type(ctor_app);
     }
+    size_t arg_count = dll_len(args);
 
-    // Extract indices from constructor return type
-    // current holds the return type after stripping foralls
+    // `current` now holds the return type `I params indices`; pull the indices out
+    // of its application spine (the arguments after the parameters).
     Expression **ctor_indices = NULL;
     if (index_count > 0) {
         ctor_indices = malloc(index_count * sizeof(Expression *));
-
-        // Parse the return type as a spine of applications
-        // For eq_refl: (((eq A) x) x) - we want to extract the indices (the
-        // trailing applications)
         DoublyLinkedList *spine = dll_create();
         Expression *head = current;
         while (kernel_app_func(head) != NULL) {
             dll_insert_at_head(spine, dll_new_node(kernel_app_arg(head)));
             head = kernel_app_func(head);
         }
-
-        // The spine now has all the arguments. Skip param_count, take
-        // index_count
-        size_t total_args = dll_len(spine);
-        if (total_args < param_count + index_count) {
+        if (dll_len(spine) < param_count + index_count) {
             fprintf(stderr, ERROR "Constructor return type has too few arguments\n" CRESET);
             dll_destroy(spine);
-            dll_destroy(arg_types);
-            free(arg_vars);
+            dll_destroy(args);
             free(ctor_indices);
             return NULL;
         }
-
-        // Extract the indices (skip parameters)
         for (size_t i = 0; i < index_count; i++) {
             ctor_indices[i] = (Expression *)dll_at(spine, param_count + i)->data;
         }
-
         dll_destroy(spine);
     }
 
-    // Apply motive to indices first, then to constructor application
+    // Conclusion: `P indices (c params args)`, valid in case_ctx (the innermost
+    // argument, or elim_ctx for a constructor with no arguments).
     Expression *case_result = motive_var;
     for (size_t i = 0; i < index_count; i++) {
         case_result = kernel_app_create(case_result, ctor_indices[i], case_ctx);
-        if (!case_result) {
-            fprintf(stderr, ERROR "Failed to apply motive to index %zu\n" CRESET, i);
-            dll_destroy(arg_types);
-            free(arg_vars);
-            if (ctor_indices) {
-                free(ctor_indices);
-            }
-            return NULL;
-        }
     }
-
     case_result = kernel_app_create(case_result, ctor_app, case_ctx);
+    if (ctor_indices) {
+        free(ctor_indices);
+    }
     if (!case_result) {
         fprintf(stderr, ERROR "Failed to apply motive to constructor application\n" CRESET);
-        dll_destroy(arg_types);
-        free(arg_vars);
-        if (ctor_indices) {
-            free(ctor_indices);
-        }
+        dll_destroy(args);
         return NULL;
     }
 
-    if (ctor_indices) {
-        free(ctor_indices);
-    }
     Expression *case_type = case_result;
+
+    // Wrap the conclusion with an induction hypothesis per recursive argument,
+    // giving `IH_0 -> .. -> IH_k -> P (c args)`. These sit inside the argument
+    // binders below because each hypothesis mentions its argument.
+    for (size_t i = arg_count; i > 0; i--) {
+        Expression *arg_var = (Expression *)dll_at(args, i - 1)->data;
+        Expression *hypothesis = _build_recursive_arg_hypothesis(
+            arg_var, kernel_expr_type(arg_var), ind_var, motive_var, param_count, index_count,
+            case_ctx);
+        if (hypothesis) {
+            case_type = kernel_arrow_create(hypothesis, case_type, case_ctx);
+        }
+    }
+
     for (size_t i = arg_count; i > 0; i--) {
-        case_type = kernel_forall_create(arg_vars[i - 1], case_type);
+        case_type = kernel_forall_create((Expression *)dll_at(args, i - 1)->data, case_type);
     }
 
-    dll_destroy(arg_types);
-    free(arg_vars);
+    dll_destroy(args);
     return case_type;
 }
 
@@ -792,16 +847,8 @@ static int _handle_inductive_command(MEngineRuntime *rt, InductiveCmd *ind_cmd)
     char *ind_principle_name = malloc(strlen(name) + 5);
     sprintf(ind_principle_name, "%s_ind", name);
 
-    /* The induction principle builder uses the original param_vars, but
-     * constructor types now use fresh parameter copies.  The resulting case
-     * types would fail the application type check (fresh_param != original_param).
-     * Skip the induction principle for parametric inductives; it is not needed
-     * by the tactics that use parametric types (e.g., sep_list in cancel). */
-    Expression *ind_principle_type = NULL;
-    if (param_count == 0) {
-        ind_principle_type =
-            _build_induction_principle_type(ind_cmd, ind_var, param_vars, param_count, contexts);
-    }
+    Expression *ind_principle_type =
+        _build_induction_principle_type(ind_cmd, ind_var, param_vars, param_count, contexts);
 
     Expression *ind_principle_var = NULL;
     if (ind_principle_type) {
diff --git a/src/common/map.c b/src/common/map.c
index 3d02dd72..8c9d2712 100644
--- a/src/common/map.c
+++ b/src/common/map.c
@@ -37,6 +37,19 @@ struct Map {
 
 static MapEntry *map_entries_new(size_t capacity) { return calloc(capacity, sizeof(MapEntry)); }
 
+// All slot indexing masks with `capacity - 1`, so the capacity must be a power
+// of two (otherwise the probe sequence skips slots and a lookup of an absent key
+// in a full table loops forever).  map_new uses a power-of-two literal and resize
+// doubles, but map_new_with_capacity takes a caller-supplied size (e.g. a match's
+// pattern-variable count), so round it up to the next power of two, floor 1.
+static size_t map_round_capacity(size_t requested) {
+    size_t cap = 1;
+    while (cap < requested) {
+        cap <<= 1;
+    }
+    return cap;
+}
+
 // Size+tombstones together determine slot pressure.
 static bool map_should_grow(Map *m) {
     return (m->size + m->tombstones + 1) * MAP_LOAD_FACTOR_DEN > m->capacity * MAP_LOAD_FACTOR_NUM;
@@ -100,7 +113,7 @@ Map *map_new_with_capacity(size_t initial_capacity) {
     if (!m) {
         return NULL;
     }
-    m->capacity = initial_capacity;
+    m->capacity = map_round_capacity(initial_capacity);
     m->size = 0;
     m->tombstones = 0;
     m->entries = map_entries_new(m->capacity);
diff --git a/src/engine/rewrite_internal.c b/src/engine/rewrite_internal.c
index fa7a9b26..af39ca9c 100644
--- a/src/engine/rewrite_internal.c
+++ b/src/engine/rewrite_internal.c
@@ -358,8 +358,13 @@ RewriteResult *rewrite_head(Expression *mid, Expression *lemma, Context *context
     }
 
     Expression *proof = unif_result->lemma_instantiation;
-    Expression *proof_type = kernel_expr_type(proof);
-    if (!kernel_expr_congruent(_get_lhs_eq(proof_type), mid)) {
+    // Normalize the proof's type before reading off its equality: an induction
+    // hypothesis arrives as a beta-redex `(motive) x` (the eliminator's `P x`), so
+    // whnf exposes the underlying eq. Without this _get_lhs_eq returns NULL and the
+    // congruence check below dereferences it.
+    Expression *proof_type = kernel_normalize_whnf(kernel_expr_type(proof));
+    Expression *lhs = _get_lhs_eq(proof_type);
+    if (!lhs || !kernel_expr_congruent(lhs, mid)) {
         free_unification_result(unif_result);
         return init_rewrite_result(mid, mid, NULL, NULL);
     }
diff --git a/src/engine/unify.c b/src/engine/unify.c
index 037b40c0..1112112d 100644
--- a/src/engine/unify.c
+++ b/src/engine/unify.c
@@ -205,7 +205,11 @@ UnificationResult *eunify2(Expression *lemma, Expression *goal) {
 
 UnificationResult *bad_unify_for_eq(Context *goal_context, Expression *lemma, Expression *expr) {
     Expression *current_lemma_app = lemma;
-    Expression *current_lemma_app_ty = kernel_expr_type(current_lemma_app);
+    // Normalize the lemma type before inspecting it: an induction hypothesis arrives
+    // as a beta-redex `(motive) x` (the eliminator's `P x`) whose whnf is the actual
+    // `forall ... eq ...`. Without this the foralls stay hidden behind the redex and
+    // never get instantiated, so the rewrite finds nothing to do.
+    Expression *current_lemma_app_ty = kernel_normalize_whnf(kernel_expr_type(current_lemma_app));
     DoublyLinkedList *remaining_open = dll_create();
     while (kernel_expr_is_forall(current_lemma_app_ty)) {
         Expression *current_lemma_ty_lhs =
@@ -229,7 +233,7 @@ UnificationResult *bad_unify_for_eq(Context *goal_context, Expression *lemma, Ex
             dll_destroy(remaining_open);
             return NULL;
         }
-        current_lemma_app_ty = kernel_expr_type(current_lemma_app);
+        current_lemma_app_ty = kernel_normalize_whnf(kernel_expr_type(current_lemma_app));
     }
     return init_unification_result(current_lemma_app, remaining_open);
 }
diff --git a/src/kernel/conversion.c b/src/kernel/conversion.c
index 5eaca3a3..7452f6eb 100644
--- a/src/kernel/conversion.c
+++ b/src/kernel/conversion.c
@@ -281,16 +281,14 @@ static Expression *conversion_whnf(Expression *expr) {
                     }
                 }
 
-                if (norm_func->tag == FIX_EXPRESSION && is_fix_reducible(norm_func)) {
-                    Expression *unfolded = fix_reduce(norm_func);
-                    if (unfolded) {
-                        Expression *next = init_app_expression_wc(unfolded, arg, ctx);
-                        if (next) {
-                            conversion_record_step(ctx, current, next, CONVERSION_FIX);
-                            current = next;
-                            continue;
-                        }
-                    }
+                // Reduce a fix at the head of the spine only when its decreasing
+                // argument is constructor-headed (guards against non-termination on
+                // symbolic recursive arguments).
+                Expression *fix_unfolded = fix_reduce_app(current, conversion_whnf);
+                if (fix_unfolded) {
+                    conversion_record_step(ctx, current, fix_unfolded, CONVERSION_FIX);
+                    current = fix_unfolded;
+                    continue;
                 }
 
                 conversion_record_whnf(current, current);
@@ -299,15 +297,8 @@ static Expression *conversion_whnf(Expression *expr) {
             }
 
             case FIX_EXPRESSION: {
-                if (is_fix_reducible(current)) {
-                    Expression *next = fix_reduce(current);
-                    if (next) {
-                        conversion_record_step(get_expression_context(current), current, next,
-                                               CONVERSION_FIX);
-                        current = next;
-                        continue;
-                    }
-                }
+                // A bare fix is a value; it reduces only once applied to a
+                // constructor-headed decreasing argument (handled in APP_EXPRESSION).
                 conversion_record_whnf(current, current);
                 conversion_record_whnf(start, current);
                 return current;
diff --git a/src/kernel/expression.c b/src/kernel/expression.c
index 972e8ffe..c0982d4b 100644
--- a/src/kernel/expression.c
+++ b/src/kernel/expression.c
@@ -1,6 +1,7 @@
 #include "src/kernel/expression.h"
 
 #include <stdbool.h>
+#include <stdint.h>
 #include <stdio.h>
 #include <stdlib.h>
 #include <string.h>
@@ -193,8 +194,78 @@ void free_expression_graph(Expression *root) { (void)root; }
 
 void free_filled_hole(Expression *hole) { (void)hole; }
 
-// Flat free of a single expression's non-expression heap allocations.
-static void gc_free_node(Expression *expr) {
+/* Pointer set used at shutdown to free each shared sub-allocation exactly once.
+   MATCH branch arrays (and their MatchBranch structs / pattern-variable arrays)
+   and FIX argument arrays are shared by pointer across distinct arena nodes —
+   e.g. normalize/conversion rebuild a match with a new scrutinee but reuse the
+   original branches array.  A naive per-node free would double-free them. */
+typedef struct {
+    uintptr_t *slots;
+    size_t capacity;
+    size_t count;
+} PtrSet;
+
+static void ptrset_init(PtrSet *set) {
+    set->capacity = 1024;
+    set->count = 0;
+    set->slots = calloc(set->capacity, sizeof(uintptr_t));
+}
+
+static void ptrset_free(PtrSet *set) {
+    free(set->slots);
+    set->slots = NULL;
+    set->capacity = 0;
+    set->count = 0;
+}
+
+static size_t ptrset_slot(uintptr_t key, size_t mask) {
+    return (size_t)((key >> 4) ^ (key >> 12)) & mask;
+}
+
+static void ptrset_grow(PtrSet *set) {
+    uintptr_t *old_slots = set->slots;
+    size_t old_capacity = set->capacity;
+    set->capacity *= 2;
+    set->slots = calloc(set->capacity, sizeof(uintptr_t));
+    size_t mask = set->capacity - 1;
+    for (size_t i = 0; i < old_capacity; i++) {
+        if (!old_slots[i]) {
+            continue;
+        }
+        size_t idx = ptrset_slot(old_slots[i], mask);
+        while (set->slots[idx]) {
+            idx = (idx + 1) & mask;
+        }
+        set->slots[idx] = old_slots[i];
+    }
+    free(old_slots);
+}
+
+// Returns true if ptr was newly inserted, false if it was already present.
+static bool ptrset_insert(PtrSet *set, const void *ptr) {
+    if (!ptr) {
+        return false;
+    }
+    if ((set->count + 1) * 10 >= set->capacity * 7) {
+        ptrset_grow(set);
+    }
+    uintptr_t key = (uintptr_t)ptr;
+    size_t mask = set->capacity - 1;
+    size_t idx = ptrset_slot(key, mask);
+    while (set->slots[idx]) {
+        if (set->slots[idx] == key) {
+            return false;
+        }
+        idx = (idx + 1) & mask;
+    }
+    set->slots[idx] = key;
+    set->count++;
+    return true;
+}
+
+// Flat free of a single expression's non-expression heap allocations.  Shared
+// sub-allocations are guarded by `freed` so each is released exactly once.
+static void gc_free_node(Expression *expr, PtrSet *freed) {
     /* Uplink nodes are arena-managed; no per-node free needed. */
     expr->uplinks = NULL;
 
@@ -205,15 +276,21 @@ static void gc_free_node(Expression *expr) {
             free(expr->as.var.name);
             break;
         case MATCH_EXPRESSION:
-            for (int i = 0; i < expr->as.match.branch_count; i++) {
-                MatchBranch *branch = expr->as.match.branches[i];
-                free(branch->pattern_variables);
-                free(branch);
+            if (ptrset_insert(freed, expr->as.match.branches)) {
+                for (int i = 0; i < expr->as.match.branch_count; i++) {
+                    MatchBranch *branch = expr->as.match.branches[i];
+                    if (ptrset_insert(freed, branch)) {
+                        free(branch->pattern_variables);
+                        free(branch);
+                    }
+                }
+                free(expr->as.match.branches);
             }
-            free(expr->as.match.branches);
             break;
         case FIX_EXPRESSION:
-            free(expr->as.fix.args);
+            if (ptrset_insert(freed, expr->as.fix.args)) {
+                free(expr->as.fix.args);
+            }
             break;
         case HOLE_EXPRESSION:
             free(expr->as.hole.name);
@@ -228,15 +305,18 @@ void expression_gc_shutdown(void) {
     inductive_registry_shutdown();
     conversion_cache_clear();
 
+    PtrSet freed;
+    ptrset_init(&freed);
     ExprArenaPage *page = g_arena_pages;
     while (page) {
         ExprArenaPage *next = page->next;
         for (int i = 0; i < page->used; i++) {
-            gc_free_node(&page->nodes[i]);
+            gc_free_node(&page->nodes[i], &freed);
         }
         free(page);
         page = next;
     }
+    ptrset_free(&freed);
     g_arena_pages = NULL;
     g_arena_current = NULL;
 
@@ -453,11 +533,11 @@ Expression *init_app_expression_wc(Expression *func, Expression *arg, Context *c
         return NULL;
     }
 
-    Expression *func_type = get_expression_type(func);
-    if (func_type->tag != FORALL_EXPRESSION) {
-        fprintf(stderr, ERROR "Function is not a Forall expression.\n" CRESET);
-        return NULL;
-    }
+    // Whether `func`'s type is a Pi is validated by _construct_app_type below, which
+    // weak-head-normalizes first. That matters for functions whose type is a Pi only
+    // up to reduction (e.g. an induction hypothesis typed by the eliminator's
+    // beta-redex `(motive) x`); a premature syntactic FORALL check here would reject
+    // them. _construct_app_type returns NULL (and reports) for genuine non-functions.
 
     if (!valid_in_context(arg, context)) {
         fprintf(stderr, ERROR "Argument is not valid in context.\n" CRESET);
@@ -811,15 +891,6 @@ Expression *init_fix_expression_wc(Expression *recursive_var, Expression **args,
         }
     }
 
-    Expression *body_bound = body;
-    for (int i = arg_count - 1; i >= 0; i--) {
-        body_bound = init_lambda_expression_wc(args[i], body_bound);
-        if (!body_bound) {
-            fprintf(stderr, ERROR "Failed to create body bound.\n" CRESET);
-            return NULL;
-        }
-    }
-
     Expression *expr = _init_expression_base(/* tag */ FIX_EXPRESSION, /* context */ gamma,
                                              /* ctx_size */ gamma->ctx_size,
                                              /* type */ get_expression_type(recursive_var));
@@ -841,7 +912,13 @@ Expression *init_fix_expression_wc(Expression *recursive_var, Expression **args,
     }
     propagate_evar_refs(expr, body);
 
-    if (!register_fix_body_to_expression(recursive_var, body_bound)) {
+    // Register the fix node itself as the recursive variable's definition. Unfolding
+    // the constant therefore yields a fix node (a value), so reduction is governed by
+    // the guarded fix rule (see fix_reduce_app): it fires only once the decreasing
+    // argument is constructor-headed. Registering the eta-expanded lambda form instead
+    // would make the constant delta-unfold unconditionally and loop on symbolic
+    // recursive arguments.
+    if (!register_fix_body_to_expression(recursive_var, expr)) {
         fprintf(stderr, ERROR "Failed to register body to recursive variable.\n" CRESET);
         free_expression(expr);
         return NULL;
diff --git a/src/kernel/fix_reduction.c b/src/kernel/fix_reduction.c
index 2257848d..6486c02b 100644
--- a/src/kernel/fix_reduction.c
+++ b/src/kernel/fix_reduction.c
@@ -2,7 +2,8 @@
 
 #include <stdlib.h>
 
-#include "src/kernel/subst.h"
+#include "src/kernel/delta_reduction.h"
+#include "src/kernel/inductive.h"
 
 bool is_fix_reducible(Expression *expression) { return expression->tag == FIX_EXPRESSION; }
 
@@ -11,13 +12,18 @@ Expression *fix_reduce(Expression *expression) {
         return NULL;
     }
 
-    Expression *recursive_var = get_fix_recursive_var(expression);
     Expression **args = get_fix_args(expression);
     int arg_count = get_fix_arg_count(expression);
     Expression *body = get_fix_body(expression);
-    Context *context = get_expression_context(body);
 
-    Expression *result = new_subst(context, body, recursive_var, expression);
+    // Recursive occurrences in the body refer to the fix's recursive variable, whose
+    // definitional body is this very fix node (registered in init_fix_expression_wc).
+    // So unfolding is just stripping the fix down to its lambda abstraction over the
+    // arguments; the recursive calls keep resolving through the recursive variable
+    // (via delta). Substituting the fix node inline instead would be wrong here: the
+    // fix shares its argument binders with the body, so re-binding them with the
+    // wrapping lambdas would capture the copies living inside the substituted fix.
+    Expression *result = body;
 
     for (int i = arg_count - 1; i >= 0; i--) {
         result = init_lambda_expression_wc(args[i], result);
@@ -28,3 +34,78 @@ Expression *fix_reduce(Expression *expression) {
 
     return result;
 }
+
+Expression *fix_reduce_app(Expression *app, Expression *(*whnf)(Expression *)) {
+    // The fix at the head of the application spine fires only when its decreasing
+    // argument is in constructor head normal form. This is the standard guard that
+    // keeps reduction terminating on symbolic (variable) recursive arguments:
+    // `add n O` with `n` a variable stays stuck instead of unfolding forever.
+    //
+    // The head may already be a fix node, or a constant (recursive variable) whose
+    // definition is this fix. cbv/whnf keep such constants folded so that a *stuck*
+    // residual stays constant-headed (`add n O`, not `(fix ...) n O`) and therefore
+    // matchable by rewrite/congruence; we unfold here only to govern firing.
+    Expression *head = get_head(app);
+    Expression *fix = NULL;
+    if (head->tag == FIX_EXPRESSION) {
+        fix = head;
+    } else if (head->tag == VAR_EXPRESSION && is_delta_reducible(head)) {
+        Expression *body = delta_reduce(head);
+        if (body && body->tag == FIX_EXPRESSION) {
+            fix = body;
+        }
+    }
+    if (!fix) {
+        return NULL;
+    }
+
+    int decreasing_index = get_fix_decreasing_arg_index(fix);
+    if (decreasing_index < 0) {
+        return NULL;
+    }
+
+    // Count the spine arguments (app = (((fix) a0) a1) ... a_{count-1}).
+    int count = 0;
+    for (Expression *cursor = app; cursor->tag == APP_EXPRESSION; cursor = get_app_func(cursor)) {
+        count++;
+    }
+    if (decreasing_index >= count) {
+        // The decreasing argument has not been supplied yet; cannot reduce.
+        return NULL;
+    }
+
+    Expression **args = malloc(count * sizeof(Expression *));
+    if (!args) {
+        return NULL;
+    }
+    Expression *cursor = app;
+    for (int i = count - 1; i >= 0; i--) {
+        args[i] = get_app_arg(cursor);
+        cursor = get_app_func(cursor);
+    }
+
+    Expression *decreasing_arg = whnf ? whnf(args[decreasing_index]) : args[decreasing_index];
+    if (!is_constructor(get_head(decreasing_arg))) {
+        free(args);
+        return NULL;
+    }
+
+    Expression *unfolded = fix_reduce(fix);
+    if (!unfolded) {
+        free(args);
+        return NULL;
+    }
+
+    Context *context = get_expression_context(app);
+    Expression *result = unfolded;
+    for (int i = 0; i < count; i++) {
+        result = init_app_expression_wc(result, args[i], context);
+        if (!result) {
+            free(args);
+            return NULL;
+        }
+    }
+
+    free(args);
+    return result;
+}
diff --git a/src/kernel/fix_reduction.h b/src/kernel/fix_reduction.h
index 843248d3..2f8fd438 100644
--- a/src/kernel/fix_reduction.h
+++ b/src/kernel/fix_reduction.h
@@ -24,4 +24,16 @@ bool is_fix_reducible(Expression *expression);
 // where gamma is the context which the fix expression is well-typed in.
 Expression *fix_reduce(Expression *expression);
 
-#endif  // FIX_REDUCTION_H
\ No newline at end of file
+// fix_reduce_app reduces an application `(((fix ...) a0) a1) ... an` whose head is a
+// fix, but only when the guard condition holds: the decreasing argument (after being
+// reduced to weak head normal form via `whnf`) is in constructor head normal form.
+// This mirrors Coq's iota/fix rule and prevents non-termination when a fixpoint is
+// applied to a symbolic (variable) recursive argument.
+//
+// Returns the unfolded-and-reapplied term on success, or NULL when `app` is not a
+// fix application, the decreasing argument has not been supplied, or it is not
+// constructor-headed (i.e. the redex is stuck). `whnf` may be NULL to skip reducing
+// the decreasing argument (useful when the caller has already normalized it).
+Expression *fix_reduce_app(Expression *app, Expression *(*whnf)(Expression *));
+
+#endif  // FIX_REDUCTION_H
diff --git a/src/kernel/mixed_subst.c b/src/kernel/mixed_subst.c
index 5c6669db..db1d2171 100644
--- a/src/kernel/mixed_subst.c
+++ b/src/kernel/mixed_subst.c
@@ -369,10 +369,24 @@ static Expression *_simple_topdown_psubst(Context *ctx, Expression *t, Map *subs
                     Expression *old_var_type = get_expression_type(old_var);
                     Expression *new_var_type =
                         _simple_topdown_psubst(branch_ctx, old_var_type, subst_map, NULL);
+                    // A parameter-slot pattern variable of a parametric inductive
+                    // carries a delta-reducible body (the type argument read off the
+                    // scrutinee, e.g. `_ := A`).  Preserve it: dropping the alias here
+                    // makes later pattern variables' types (`x : _`, `xs : list _`)
+                    // opaque, so rebuilding the branch body's applications fails to
+                    // type-check.
+                    Expression *old_var_body = get_var_body(old_var);
+                    Expression *new_var_body =
+                        old_var_body
+                            ? _simple_topdown_psubst(branch_ctx, old_var_body, subst_map, NULL)
+                            : NULL;
                     Expression *new_var;
-                    if (new_var_type == old_var_type &&
+                    if (new_var_type == old_var_type && new_var_body == old_var_body &&
                         branch_ctx == get_expression_context(old_var)) {
                         new_var = old_var;
+                    } else if (old_var_body) {
+                        new_var = init_var_expression_wc_with_body(get_var_name(old_var),
+                                                                   new_var_body, branch_ctx);
                     } else {
                         new_var =
                             init_var_expression_wc(get_var_name(old_var), new_var_type, branch_ctx);
@@ -630,8 +644,19 @@ static Expression *spine_rebuild(Context *apps_ctx, Expression *node, Map *subst
                     Expression *old_var = br->pattern_variables[j];
                     Expression *new_var_type = maybe_rebuild(apps_ctx, get_expression_type(old_var),
                                                              subst_map, memo, subtree_gen);
-                    Expression *new_var =
-                        init_var_expression_wc(get_var_name(old_var), new_var_type, apps_ctx);
+                    // Preserve a parameter-slot pattern variable's delta-reducible
+                    // body (see the matching note in _simple_topdown_psubst).
+                    Expression *old_var_body = get_var_body(old_var);
+                    Expression *new_var;
+                    if (old_var_body) {
+                        Expression *new_var_body =
+                            maybe_rebuild(apps_ctx, old_var_body, subst_map, memo, subtree_gen);
+                        new_var = init_var_expression_wc_with_body(get_var_name(old_var),
+                                                                   new_var_body, apps_ctx);
+                    } else {
+                        new_var =
+                            init_var_expression_wc(get_var_name(old_var), new_var_type, apps_ctx);
+                    }
                     br2->pattern_variables[j] = new_var;
                     if (new_var != old_var) {
                         map_set(subst_map, old_var, new_var);
diff --git a/src/kernel/normalize.c b/src/kernel/normalize.c
index 8f80a7f3..64ed76dc 100644
--- a/src/kernel/normalize.c
+++ b/src/kernel/normalize.c
@@ -39,15 +39,35 @@ static Expression *_normalize_cbv(Expression *expr, ReductionFlags flags) {
                     }
                 }
 
-                // Rebuild application if subexpressions changed
+                // Rebuild the application with normalized subexpressions (the args
+                // are now values, since cbv normalizes them first).
+                Expression *rebuilt = current;
                 if (norm_func != func || norm_arg != arg) {
-                    next = init_app_expression_wc(norm_func, norm_arg, ctx);
-                    if (next) {
-                        current = next;
+                    rebuilt = init_app_expression_wc(norm_func, norm_arg, ctx);
+                    if (!rebuilt) {
+                        break;
+                    }
+                }
+
+                // Guarded fix reduction on an applied fixpoint (mirrors
+                // normalize_whnf): unfold `(fix ...) args` one step only when the
+                // decreasing argument is constructor-headed, so the surrounding match
+                // can then iota-reduce. The guard prevents runaway unfolding on a
+                // symbolic recursive argument.
+                if (flags & REDUCE_FIX) {
+                    Expression *unfolded = fix_reduce_app(rebuilt, normalize_whnf);
+                    if (unfolded) {
+                        current = unfolded;
                         changed = true;
                         continue;
                     }
                 }
+
+                if (rebuilt != current) {
+                    current = rebuilt;
+                    changed = true;
+                    continue;
+                }
                 break;
             }
 
@@ -55,6 +75,14 @@ static Expression *_normalize_cbv(Expression *expr, ReductionFlags flags) {
                 // Try delta reduction if enabled
                 if ((flags & REDUCE_DELTA) && is_delta_reducible(current)) {
                     next = delta_reduce(current);
+                    if (next && next->tag == FIX_EXPRESSION) {
+                        // A constant whose definition is a fixpoint is a value here; it
+                        // fires only when applied to a constructor-headed decreasing
+                        // argument (handled in the APP case via fix_reduce_app). Holding
+                        // it folded keeps a stuck residual constant-headed (`add n O`,
+                        // not `(fix ...) n O`) so rewrite/congruence can match it.
+                        return current;
+                    }
                     if (next) {
                         // Continue normalizing the unfolded definition
                         current = next;
@@ -67,17 +95,8 @@ static Expression *_normalize_cbv(Expression *expr, ReductionFlags flags) {
             }
 
             case FIX_EXPRESSION: {
-                // Try fix reduction if enabled
-                if ((flags & REDUCE_FIX) && is_fix_reducible(current)) {
-                    next = fix_reduce(current);
-                    if (next) {
-                        // Continue normalizing the result of fix reduction
-                        current = next;
-                        changed = true;
-                        continue;
-                    }
-                }
-                // FIX expressions that can't be reduced are in normal form
+                // A bare fix is a value; it reduces only once applied to a
+                // constructor-headed decreasing argument (see the APP case).
                 return current;
             }
 
@@ -157,6 +176,12 @@ Expression *normalize_whnf(Expression *expr) {
             case VAR_EXPRESSION: {
                 if (is_delta_reducible(current)) {
                     Expression *next = delta_reduce(current);
+                    if (next && next->tag == FIX_EXPRESSION) {
+                        // Fixpoint constant: a value here, fires in the APP case via
+                        // fix_reduce_app. Holding it folded keeps stuck residuals
+                        // constant-headed and matchable (see _normalize_cbv).
+                        return current;
+                    }
                     if (next) {
                         current = next;
                         continue;
@@ -183,25 +208,21 @@ Expression *normalize_whnf(Expression *expr) {
                     continue;
                 }
 
-                if (norm_func->tag == FIX_EXPRESSION && is_fix_reducible(norm_func)) {
-                    Expression *unfolded = fix_reduce(norm_func);
-                    if (unfolded) {
-                        current = init_app_expression_wc(unfolded, arg, ctx);
-                        continue;
-                    }
+                // Guarded fix reduction: only fire when the decreasing argument is
+                // constructor-headed (see fix_reduce_app), preventing runaway
+                // unfolding on symbolic recursive arguments.
+                Expression *fix_unfolded = fix_reduce_app(current, normalize_whnf);
+                if (fix_unfolded) {
+                    current = fix_unfolded;
+                    continue;
                 }
 
                 return current;
             }
 
             case FIX_EXPRESSION: {
-                if (is_fix_reducible(current)) {
-                    Expression *next = fix_reduce(current);
-                    if (next) {
-                        current = next;
-                        continue;
-                    }
-                }
+                // A bare fix is a value; reduction happens in APP_EXPRESSION once a
+                // constructor-headed decreasing argument is applied.
                 return current;
             }
 
diff --git a/src/kernel/type_compat.c b/src/kernel/type_compat.c
index ad4971b2..54bbae79 100644
--- a/src/kernel/type_compat.c
+++ b/src/kernel/type_compat.c
@@ -40,6 +40,18 @@ static bool _open_compat(Expression *expected, Expression *actual, Map *bv_map,
     }
 
     if (actual->tag == HOLE_EXPRESSION) {
+        // Symmetric to the expected-side case: a hole on the actual (term-type) side is
+        // an unsolved evar that must be instantiated to `expected` for the term's type
+        // to match. This occurs when applying a function whose result type is a
+        // beta-redex that whnf-reduces to a binder (e.g. an eliminator's `motive y0`
+        // with a quantified motive): the index `y0` cannot be solved by spine
+        // unification and ends up embedded in the term type as a hole. Recording the
+        // assignment lets fill_hole cascade-fill it instead of leaving a stray goal.
+        Expression *already_mapped = linear_map_get(holes, actual);
+        if (already_mapped != NULL) {
+            return _open_compat(expected, already_mapped, bv_map, holes);
+        }
+        linear_map_set(holes, actual, expected);
         return _open_compat(get_expression_type(expected), get_expression_type(actual), bv_map,
                             holes);
     }
diff --git a/src/runtime/core.c b/src/runtime/core.c
index 1cdc9074..45297a9b 100644
--- a/src/runtime/core.c
+++ b/src/runtime/core.c
@@ -468,8 +468,17 @@ static Context *init_bad_app_congruence(Context *c) {
 }
 
 Expression *_get_lhs_eq(Expression *eq_expression) {
-    // eq_expression is of the form eq A x y
-    return kernel_app_arg(kernel_app_func(eq_expression));
+    // eq_expression is of the form `eq A x y`; return NULL when it is not a fully
+    // applied equality (e.g. a partially-applied or non-eq type), so callers fail
+    // cleanly instead of dereferencing a missing application argument.
+    if (!eq_expression || !kernel_expr_is_app(eq_expression)) {
+        return NULL;
+    }
+    Expression *eq_app = kernel_app_func(eq_expression);
+    if (!eq_app || !kernel_expr_is_app(eq_app)) {
+        return NULL;
+    }
+    return kernel_app_arg(eq_app);
 }
 
 Expression *_get_rhs_eq(Expression *eq_expression) {
diff --git a/src/runtime/runtime.c b/src/runtime/runtime.c
index b14936a6..c8df46c1 100644
--- a/src/runtime/runtime.c
+++ b/src/runtime/runtime.c
@@ -53,10 +53,22 @@ MEngineRuntime *mengine_runtime_new(MEngineOptions *options) {
 
     rt->proof_state = NULL;
     rt->pending_theorem = NULL;
-    rt->options = options;
+
+    // Own a private copy of the options rather than borrowing the caller's
+    // pointer.  The runtime reads through rt->options for its whole life (and
+    // even mutates it transiently, e.g. the quiet toggle below), so a borrowed
+    // pointer to a caller stack local would dangle the moment that caller
+    // returns.  See bugs/note_dangling_options_pointer.md.
+    rt->options = malloc(sizeof(MEngineOptions));
+    if (!rt->options) {
+        free(rt);
+        return NULL;
+    }
+    *rt->options = *options;
 
     rt->ctx = kernel_context_empty();
     if (!rt->ctx) {
+        free(rt->options);
         free(rt);
         return NULL;
     }
@@ -110,6 +122,7 @@ void mengine_runtime_free(MEngineRuntime *rt) {
     engine_rewrite_print_cumulative_stats();
 
     kernel_context_free(rt->ctx);
+    free(rt->options);
     free(rt);
 
     kernel_expression_gc_shutdown();
diff --git a/src/tacticlanguage/tactic_interp.c b/src/tacticlanguage/tactic_interp.c
index fc6d951f..0496e454 100644
--- a/src/tacticlanguage/tactic_interp.c
+++ b/src/tacticlanguage/tactic_interp.c
@@ -849,8 +849,13 @@ TacticResult *tactic_interpret(MEngineRuntime *rt, Expression *goal, TacticExpr
                 return engine_tactic_result_new(false, NULL, "rewrite_unify: unresolved bindings");
             }
             Expression *inst = engine_unify_get_lemma(unif);
-            Expression *proof_type = kernel_expr_type(inst);
-            if (!kernel_expr_congruent(_get_lhs_eq(proof_type), target)) {
+            // Normalize the lemma type: an induction hypothesis arrives as a beta-redex
+            // `(motive) x` (the eliminator's `P x`), so reduce to expose the underlying
+            // eq before extracting its LHS. Without this _get_lhs_eq returns NULL and the
+            // congruence check dereferences it.
+            Expression *proof_type = kernel_normalize_whnf(kernel_expr_type(inst));
+            Expression *lhs = _get_lhs_eq(proof_type);
+            if (!lhs || !kernel_expr_congruent(lhs, target)) {
                 engine_unify_free(unif);
                 return engine_tactic_result_new(false, NULL,
                                                 "rewrite_unify: LHS does not match target");
diff --git a/tests/engine/test_integration.c b/tests/engine/test_integration.c
index f2e77ee3..ce513283 100644
--- a/tests/engine/test_integration.c
+++ b/tests/engine/test_integration.c
@@ -51,6 +51,23 @@ static void test_inductive_nat(void) {
            "Check nat_ind.\n");
 }
 
+/* The generated induction principle must carry an induction hypothesis for each
+ * recursive argument (not just case analysis).  This proof only type-checks if
+ * `case_S` is `forall n, P n -> P (S n)`: `step` would not match a hypothesis-
+ * free `forall n, P (S n)`. */
+static void test_induction_principle_has_ih(void) {
+    run_ok("induction principle carries the induction hypothesis",
+           "Inductive nat : Type := | O : nat | S : forall (_: nat), nat.\n"
+           "Axiom P : forall (_: nat), Prop.\n"
+           "Axiom base : P O.\n"
+           "Axiom step : forall (n : nat), forall (_: P n), P (S n).\n"
+           "Theorem allP : forall (n : nat), P n.\n"
+           "intro n.\n"
+           "apply (nat_ind P).\n"
+           "exact base.\n"
+           "exact step.\n");
+}
+
 static void test_inductive_match_pred(void) {
     run_ok("match expression: predecessor",
            "Inductive nat : Type := | O : nat | S : forall (_: nat), nat.\n"
@@ -384,12 +401,34 @@ static void test_parametric_list(void) {
            "Check cons.\n");
 }
 
+/* Parametric inductives also get an induction principle (parameters bound once,
+ * out front), with an induction hypothesis on the recursive argument. This proof
+ * only type-checks if list_ind has the shape
+ *   forall A P, P (nil A) -> (forall a l, P l -> P (cons A a l)) -> forall l, P l. */
+static void test_parametric_induction_principle(void) {
+    run_ok("parametric induction principle is usable",
+           "Inductive list (A : Type) : Type :=\n"
+           "  | nil : list A\n"
+           "  | cons : forall (_: A), forall (_: list A), list A.\n"
+           "Axiom A : Type.\n"
+           "Axiom P : forall (_: list A), Prop.\n"
+           "Axiom base : P (nil A).\n"
+           "Axiom step : forall (a : A), forall (l : list A), forall (_: P l), P (cons A a l).\n"
+           "Theorem allL : forall (l : list A), P l.\n"
+           "intro l.\n"
+           "apply (list_ind A P).\n"
+           "exact base.\n"
+           "exact step.\n");
+}
+
 void run_integration_tests(void) {
     test_suite_start("Integration Tests");
 
     test_axiom_and_check();
     test_definition();
     test_inductive_nat();
+    test_induction_principle_has_ih();
+    test_parametric_induction_principle();
     test_inductive_match_pred();
     test_inductive_bool();
     test_fixpoint_add();