eat_prods context hetype tlbody_and_type
| C.Appl _ -> raise (AssertFailure "Appl: no arguments")
| C.Const (uri,exp_named_subst) ->
eat_prods context hetype tlbody_and_type
| C.Appl _ -> raise (AssertFailure "Appl: no arguments")
| C.Const (uri,exp_named_subst) ->