The Coq mailing list

[Saulo Araujo <saulo2 AT gmail.com>]

Hi,

I am in the middle of a proof in which I need the following theorem:

Theorem strong_in_inv:

  forall E (l: list E) e f,

    In f (e :: l) -> e = f \/ (e <> f /\ In f l).

Unfortunately, I was not able to complete the proof below:

Proof.

  intros.

  simpl in H.

  destruct H.

  {

    left.

    apply H.

  }

  {

    right.

    split.

    {

(* I am stuck here! *)

    }

    {

      apply H.

    }

  }

Qed.