Error:
Illegal application:
The term "ty_syn_ch_func_clause_17_clause_1_clause_1_ty_defs_func_ind" of type
 "forall (DS : decs) (ds : defs) (x : atom),
  def_dec_maps (open x ds) (open x DS) ->
  forall (G : env) (tm : typing_mode),
  (fun v : atom =>
   v
   `notin` union
             (union (dom G)
                (union (fv_values fv_typ G) (union (fv_decs DS) (fv_defs ds))))
             match tm with
             | inl V => AtomSetProperties.of_list V
             | inr T => fv T
             end) x ->
  forall (x0 : atom) (ds' : defs) (DS' : decs),
  env -> def_dec_maps ds' DS' -> tail_of ds' (open x0 ds) -> TcE unit -> Prop"
cannot be applied to the terms
 "DS" : "decs"
 "ds" : "defs"
 "x" : "atom"
 "m" : "def_dec_maps (open x ds) (open x DS)"
 "G" : "env"
 "tm" : "typing_mode"
 "wildcard"
   : "x
      `notin` union
                (union (dom G)
                   (union (fv_values fv_typ G) (union (fv_decs DS) (fv_defs ds))))
                match tm with
                | inl V => AtomSetProperties.of_list V
                | inr T => fv T
                end"
 "fun (x : env) (x0 : trm) (x1 : typing_mode)
    (_ : trm_struct_measure x0 < trm_struct_measure (trm_val ([DS ]{ ds}))) =>
  ty_syn_ch_func x x0 x1"
   : "env ->
      forall (x0 : trm) (x1 : typing_mode),
      trm_struct_measure x0 < trm_struct_measure (trm_val ([DS ]{ ds})) ->
      TcE (tm_result x1)"
 "ty_syn_ch_func_obligations_obligation_2 x0" : "atom"
 "ds0" : "defs"
 "DS0" : "decs"
 "G'" : "env"
 "d" : "def_dec_maps ds0 DS0"
 "ty_syn_ch_func_obligations_obligation_3 ds x0 tl"
   : "tail_of ds0 (open (ty_syn_ch_func_obligations_obligation_2 x0) ds)"
 "ty_syn_ch_func_clause_17_clause_1_clause_1_ty_defs_func m G tm wildcard
    (fun (x : env) (x0 : trm) (x1 : typing_mode)
       (_ : trm_struct_measure x0 < trm_struct_measure (trm_val ([DS ]{ ds}))) =>
     ty_syn_ch_func x x0 x1) (ty_syn_ch_func_obligations_obligation_2 x0) G' d
    (ty_syn_ch_func_obligations_obligation_3 ds x0 tl)" : "TcE unit"
The 8th term has type
 "env ->
  forall (x0 : trm) (x1 : typing_mode),
  trm_struct_measure x0 < trm_struct_measure (trm_val ([DS ]{ ds})) ->
  TcE (tm_result x1)" which should be coercible to "atom".