The Coq mailing list

[Edsko de Vries <devriese AT cs.tcd.ie>]

Hi,

Sorry for replying to my own message, but here is a simplified (but
self-contained) example of what I'm trying to do:

        Inductive Foo : nat -> nat -> nat -> Prop :=
          | FooBase : Foo 0 1 2
          | FooExchange : forall (m n o:nat), Foo m n o -> Foo n m o.
        
        Lemma not_Foo : ~ (Foo 1 2 3).
        Proof.
        unfold not ; intros.

At this point, we get

        1 subgoal
        H : Foo 1 2 3
        ______________________________________(1/1)
        False

now when I do "inversion H; subst", we get

        1 subgoal
        H : Foo 1 2 3
        H0 : Foo 2 1 3
        ______________________________________(1/1)
        False

Now of course we can repeat this step as often we want, without getting any
further. How do I finish this proof?

Thank again,

Edsko