The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

Hi,

Is there a variant of Coq.Init.Fix_eq that allows you to prove properties about [Fix]es by well-founded induction?  That is, say that I have [Q : forall x, P x -> Type], and my goal is [Q x (@Fix A R Rwf P F x)].  If I do [rewrite Coq.Init.Fix_eq], I can then progress on my goal to the point where I am again faced with something like [Q y (@Fix A R Rwf P F y)].  Is there an induction principle for [Fix] that I can use to prove my goal?  Intuitively, as long as the function has [Acc] fuel for recursing, I can use the same fuel to keep rewriting with [Fix_eq].

Thanks,

Jason