The Coq mailing list

[Paolo Herms <paolo.herms AT cea.fr>]

You mean something like this?

  Section AccessibiltyFunctions.

    Variable A : Type.

    Variable f : A → A.

    Variable start : A.

    Inductive AccF : A → Prop :=
    | AccF_start : AccF start
    | AccF_cont a: AccF a → AccF (f a).

  End AccessibiltyFunctions.

AccF f a defines the set of elements accessible by iterating f starting from 
a.
-- 
Paolo Herms
PhD Student - CEA-LIST Software Safety Lab. / INRIA ProVal Project
Paris, France