Problem with refine tactic

gistfile1.txt

Set Implicit Arguments.

Require Import Arith List.

Definition name := nat

(***********************************************************************)
(** Definition of types.                                              **)

Inductive ty : Set :=
  | var   : name -> ty
  | nat   : ty
  | arrow : ty   -> ty -> ty.

Definition eq_name_dec (t1 t2 : name) : {t1=t2} + {t1<>t2} := eq_nat_dec t1 t2.

(** equality on types is decidable **)

Definition eq_ty_dec : forall (t1 t2 : ty), {t1 = t2} + {t1 <> t2}.
  decide equality.
  apply eq_name_dec.
Defined.

(************************************************************************)
(** definition of well formed types                                    **)

(** a context for type variables that are in the current scope         **)

Definition tyvarctx := list name.

(** membership in a context **)

Fixpoint Mem (ctx : tyvarctx) (n : name) : Prop :=
  match ctx with
    | nil       => False
    | (v :: vs) => if eq_name_dec v n then True else Mem vs n
  end.

(** membership is decidable **)

Definition member (ctx: tyvarctx) (n: name) : {Mem ctx n} + {~ Mem ctx n}.
  refine (fix f ctx n : {Mem ctx n} + {~ Mem ctx n} := 
              match ctx with
                 | nil => right _ _
                 | v :: vs => match eq_name_dec v n with
                           | left Heq => left _ _
                           | right Hneq =>
                               match f vs n with
                                 | left H => left _ _
                                 | right H => right _ _
                               end
                      end
          end).
Defined.