The Coq mailing list

[Dominique Larchey-Wendling <dominique.larchey-wendling AT loria.fr>]

Hi,

The only issue is that now with the Fixpoint, we don't have a constructor any more. So this means with this definition, I cannot induct on the proof tree of a satisfaction or apply inversion.

Well I suggest, and this is a general rule, to always write the induction principle that most fit your needs.

Hence in your case, write down the statement of the induction/elimination principle that corresponds to

your (extended) inductive definition and then prove it with the Fixpoint definition, ie by induction on the

structure of the formula.

The inversion principle can usually be proved using the induction principle.

D.