elem

Elem.v

(* https://coq.inria.fr/distrib/current/refman/Reference-Manual022.html *)
Class Eq (A : Type) := {
  eqb : A -> A -> bool ;
  eqb_leibniz : forall x y, eqb x y = true -> x = y }.

Instance Eq_nat : Eq nat :=
  { eqb x y := beq_nat x y }.
  intros. apply beq_nat_true. apply H. Qed.

Fixpoint elem {X : Type} {eq : Eq X} (x : X) (xs : list X) : bool :=
  match xs with
    | []    => false
    | y::ys => if eqb x y
               then true
               else elem x ys
  end.

Eval compute in elem 1 [].
     (* = false *)
     (* : bool *)
Eval compute in elem 1 [1].
     (* = if (let (eqb, _) := Eq_nat in eqb) 1 1 then true else false *)
     (* : bool *)
Eval compute in elem 1 [3;2;1;5].
     (* = if (let (eqb, _) := Eq_nat in eqb) 1 3 *)
     (*   then true *)
     (*   else *)
     (*    if (let (eqb, _) := Eq_nat in eqb) 1 2 *)
     (*    then true *)
     (*    else *)
     (*     if (let (eqb, _) := Eq_nat in eqb) 1 1 *)
     (*     then true *)
     (*     else if (let (eqb, _) := Eq_nat in eqb) 1 5 then true else false *)
     (* : bool *)
Eval compute in elem 3 [3;2;1;5].
     (* = if (let (eqb, _) := Eq_nat in eqb) 3 3 *)
     (*   then true *)
     (*   else *)
     (*    if (let (eqb, _) := Eq_nat in eqb) 3 2 *)
     (*    then true *)
     (*    else *)
     (*     if (let (eqb, _) := Eq_nat in eqb) 3 1 *)
     (*     then true *)
     (*     else if (let (eqb, _) := Eq_nat in eqb) 3 5 then true else false *)
     (* : bool *)

If you change Qed to Defined in your Eq_nat Instance, then everything should work like you expect.