(* 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
(* 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