Coq证明助手中依赖类型的问题

Inductive Exp : Set :=
| EConst : nat -> Exp
| EVar   : nat -> Exp
| EFun   : nat -> list Exp -> Exp.

及其良好的谓词：

Definition Env := list nat.

Inductive WF (env : Env) : Exp -> Prop :=
| WFConst : forall n,WF env (EConst n)
| WFVar   : forall n,In n env -> WF env (EVar n)
| WFFun   : forall n es,In n env ->
                         Forall (WF env) es ->
                         WF env (EFun n es).

这基本上说明必须在环境中定义每个变量和函数符号.现在,我想定义一个声明WF谓词可判定性的函数：

Definition WFDec (env : Env) : forall e,{WF env e} + {~ WF env e}.
   refine (fix wfdec e : {WF env e} + {~ WF env e} :=
             match e as e' return e = e' -> {WF env e'} + {~ WF env e'} with
             | EConst n => fun _ => left _ _
             | EVar n => fun _ =>
                      match in_dec eq_nat_dec n env with
                      | left _ _ => left _ _ 
                      | right _ _ => right _ _                    
                      end
             | EFun n es => fun _ =>
                      match in_dec eq_nat_dec n env with
                      | left _ _ => _
                      | right _ _ => right _ _                    
                      end  
             end (eq_refl e)) ; clear wfdec ; subst ; eauto.

问题是如何声明WF谓词是否适用于EFun案例中的表达式列表.我的明显猜测是：

...  

     match Forall_dec (WF env) wfdec es with

     ...

但Coq拒绝了它,认为递归调用wfdec是不正确的.我的问题是：是否有可能在不改变表达式表示的情况下定义这种良好谓词的可判定性？

完整的工作代码位于以下gist.