The Coq mailing list

[ldou AT cs.ecnu.edu.cn]

Hi,everyone. I just meet a strange issue below:
=======================
Require Import String Bool ListSet List Classical.
Open Scope nat_scope.
Open Scope type_scope.
Open Scope string_scope.
Open Scope list_scope.
Definition e:=string.
Definition t := list e.
Definition o := set t.
Definition m:=set o.

Definition o_dec:forall (a b:o) ,{a = b} + {a <> b}.
   repeat decide equality.
Defined.

Inductive Diag:Set :=
 DE: e->Diag.

Fixpoint interp (D:Diag) {struct D}: m  :=
match D with
|DE e => ((e::nil)::nil)::nil
end.

Lemma test: set_mem o_dec 
   (("e0" :: nil) :: nil) ((("e0" :: nil) :: nil) ::nil)=true.
Proof.
  simpl. auto.
Qed.

Lemma existselement:forall d:Diag,
  exists o':o, set_mem  o_dec o' (interp d )=true.
Proof.
  intro d.
  induction d. simpl.
=============
the problem is :when do simpl in existselement, the result turns out to be:
exists o' : o, (if o_dec o' ((e0 :: nil) :: nil) then true else false) = true
but it should be :
exists o' : o, (if o_dec o' ((("e0" :: nil) :: nil) ::nil) then true else false) = true
Why is that?