The Coq mailing list

[Randy Pollack <rpollack0 AT gmail.com>]

Page 134 of the reference manual (8.5pl2) describes the reduction rule
for a fixpoint application:

================================
The reduction for fixpoints is:
   [...]
when aki starts with a constructor. This last restriction is needed in
order to keep strong normalization.
==================================

Is is known if this last restriction is needed when the context in
which the fixpoint application is well typed doesn't contain any
axioms?  (References or examples?)

What about for specific axioms, such as functional extensionality, axiom K, 
...?

Thanks,
--Randy