Doubt about dependent pattern matching

gistfile1.coq

Inductive Kind : Set :=
  | Star : Kind
  | KFun : Kind -> Kind -> Kind.

Definition eq_kind_dec : forall (k k' : Kind), {k = k'} + {k <> k'}.
  decide equality.
Defined.

Notation ":*" := Star.
Notation "k '==>' k'" := (KFun k k') (at level 60, right associativity).

Definition VarCtx := list Kind.
Definition ConCtx := list Kind.

(* type definition *)

Inductive Elem {A : Type} : A -> list A -> Type :=
  | here  : forall x xs, Elem x (x :: xs)
  | there : forall x y xs, Elem x xs -> Elem x (y :: xs).

Inductive Ty (C : ConCtx) (V : VarCtx) : Kind -> Set :=
  | var : forall k, Elem k V -> Ty C V k
  | con : forall k, Elem k C -> Ty C V k
  | app : forall k k', Ty C V (k ==> k') -> Ty C V k -> Ty C V k'.


Definition rem : forall {k}(V : VarCtx), Elem k V -> VarCtx.
  intro k.
  refine (fix rem (V : VarCtx) : Elem k V -> VarCtx :=
            match V with
              | nil =>  fun Hx => _
              | (x :: xs) =>  fun Hx => 
                   match eq_kind_dec x k with
                     | left _ => xs
                     | right _ => rem xs _
                   end
            end) ; clear rem ; 
           try (match goal with
                  | [H : Elem _ _ |- _] => inverts* H
                end). 
Defined.

Definition weak {k k' : Kind}{V : VarCtx} (x : Elem k V) (v : Elem k' (rem x)) :  Elem k' V.
  Hint Constructors Elem.
  induction x ; simpl in v ; 
  try repeat (match goal with
                | [H : context[eq_kind_dec ?x ?y] |- _] => destruct (eq_kind_dec x y) ; substs ; auto
                | [H : ?x <> ?x |- _] => elim H ; auto
              end). 
Defined.  

Inductive EqVar {V} : forall {k k' : Kind}, Elem k V -> Elem k' V -> Prop :=
  | same : forall {k}{x : Elem k V}, EqVar x x
  | diff  : forall {k k'}(x : Elem k V)(v : Elem k' (rem x)), EqVar x (weak x v).


Definition eqVarDec {k k' V}(x : Elem k V)(v : Elem k' V) : EqVar x v.
  generalize dependent v ; generalize dependent x.
  refine (fix eqVarDec (x : Elem k V) (v : Elem k' V) : EqVar x v := 
            (match x as x' return forall (v : Elem k' V), EqVar x' v with
               | here _ _ => 
                 match v as v' return EqVar x v' with --- here x' is not visible...
                   | here _ _      => here _ _
                   | there _ _ _ _ => there _ _ _ _
                 end
               | there _ _ _ a =>
                 match v as v' return EqVar x v' with
                   | here _ _      => there _ _ _ _
                   | there _ _ _ b => there _ _ _ (eqVarDec a b)
                 end
             end) v ).