diff --git a/design/contracts/0012-tail-calls.md b/design/contracts/0012-tail-calls.md
index 54c88e7..0eb523d 100644
--- a/design/contracts/0012-tail-calls.md
+++ b/design/contracts/0012-tail-calls.md
@@ -19,12 +19,17 @@ Solution: explicit, verified tail calls.
 - **Typecheck.** A new pass `verify_tail_positions(fn_body)`
   runs after the main type-check. It walks the body with an
   `is_tail_context: bool` threaded down. The flag is `true` at
-  the start, `true` for the body of every `Term::Match` arm,
-  `true` for the right operand of `Term::Seq`, `true` for the
-  body of `Term::Let`, `true` for the body of `Term::Lam` (each
-  Lam opens its own tail scope). The flag is `false` for: args
-  of any `App`/`Do`/`Ctor`, scrutinee of `Match`, left of
-  `Seq`, condition of `Let`-bound expression. When the walker
+  the start and propagates to every sub-term that is the value of
+  the whole expression: the body of every `Term::Match` arm, both
+  branches of `Term::If`, the right operand of `Term::Seq`, the
+  body of `Term::Let` and the in-clause of `Term::LetRec`, and the
+  body of `Term::Lam` (each Lam opens its own tail scope); the
+  identity nodes `Term::Clone` / `Term::ReuseAs` and a `Term::Loop`
+  body propagate the enclosing flag unchanged. The flag is `false`
+  for every argument position: args of any
+  `App`/`Do`/`Ctor`/`Recur`/`New`, the scrutinee of `Match`, the
+  condition of `If`, the left operand of `Seq`, and the value of a
+  `Let`/`LetRec` binding. When the walker
   visits an `App { tail: true }` or `Do { tail: true }`, the
   flag must be `true` at that visit; otherwise emit diagnostic
   `tail-call-not-in-tail-position`.