The Coq mailing list

[Saulo Araujo <saulo2 AT gmail.com>]

Hi,

I am trying to prove the following very simple theorem:

Require Import Arith.

Require Import List. Import ListNotations.

Inductive OBJ := Obj : nat -> OBJ.

Definition objEq obj obj' := let 'Obj id := obj 

  in let 'Obj id' := obj' 

  in beq_nat id id'.

Fixpoint containsObj objs obj := match objs with

    | [] => false

    | obj' :: objs' => if objEq obj' obj then true else containsObj objs' obj

  end.

Theorem containsObj_t1 :

  forall (obj obj' : OBJ) (objs : list OBJ), 

  containsObj (obj :: objs) obj' = false -> containsObj objs obj' = false.

When I try

Proof.

  intros.

  simpl in H.

Qed.

Coq shows that H is

(if objEq obj obj' then true else containsObj objs obj') = false

From where I believe it is safe to say that containsObj objs obj' = false. 

But no matter what I try, I cannot convince Coq that containsObj objs obj' = false :)

Any suggestions?

Thanks in advance,

Saulo