The Coq mailing list

[Arthur Azevedo de Amorim <arthur.aa AT gmail.com>]

As a matter of fact, we can even show that any type E that satisfies your original formulation has decidable equality:

Theorem strong_in_inv_implies_eq_dec :

  forall E,

    (forall (l: list E) e f,

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

    forall x y : E, x = y \/ x <> y.

Proof.

  intros E H x y.

  destruct (H [y] x y (or_intror (or_introl (eq_refl y)))) as [H' | [H' _]]; eauto.

Qed.

Em seg, 22 de fev de 2016 às 12:27, Saulo Araujo <saulo2 AT gmail.com> escreveu:

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.