I am trying to formalize the Church-Rosser theorem for the untyped-lambda calculus. There are actually multiple such theorems, depending on whether one is considering only beta-reduction, or beta- and eta-reduction, or something more exotic. I would like my implementation to be parameterized so that I can reuse it across different reduction modalities.

I am following Selinger’s lecture notes, which explains the classic proof due to Tait and Martin-Löf. The step on page 35 is to implement the *maximal one-step parallel reduction* operation.

This operation can be explained as follows: if the term under examination is amenable to the reduction(s) being considered (eta, beta, both, …) then first recurse on the subterms, and then perform a reduction on the result. Otherwise, immediately recurse on the subterms.

Implementing this in such a way that the reduction is pluggable requires passing a callback to the reduction function. Here is a sketch implementation for beta reduction:

```
(* Perform beta reduction, and call the continuation on the resulting subterms.*)
Definition subst (cont: Term -> Term) (t: Term): option Term :=
match t with
| (\t1) $$ t2 => Some(subst (cont t1) (cont t2))
| _ => None
end.
Section reduction.
Hypothesis op: (Term -> Term) -> Term -> option Term.
Definition maximal_parallel_reduction: Term -> Term :=
fix f (t: Term) :=
match op f t with
| Some t' => t'
| None =>
match t with
| Var n => Var n
| t1 $$ t2 => (f t1) $$ (f t2)
| \t' => \(f t')
end
end.
End reduction.
```

Now Coq’s checks for well-founded recursion don’t agree with the call `op f t`

. I’ve never had to deal with non-trivial recursion in Coq. Is my best guess to work with `well_founded`

?