+ (* empty context is ok for term since it wont be used by apply_subst *)
+ (* hack: since we do not know the context and the type of term, we
+ create a substitution with cc =[] and type = Implicit; they will be
+ in any case dropped by apply_subst, but it would be better to rewrite
+ the code. Cannot we just use apply_subst_metasenv, etc. ?? *)
+ let subst_in = CicMetaSubst.apply_subst [meta,([], term,Cic.Implicit None)] in