+(* refine_meta_with_brand_new_metasenv meta term apply_subst_replacing *)
+(* newmetasenv *)
+(* This (heavy) function must be called when a tactic can instantiate old *)
+(* metavariables (i.e. existential variables). It substitues the metasenv *)
+(* of the proof with the result of removing [meta] from the domain of *)
+(* [newmetasenv]. Then it replaces Cic.Meta [meta] with [term] everywhere *)
+(* in the current proof. Finally it applies [apply_subst_replacing] to *)
+(* current proof. *)
+(*CSC: A questo punto perche' passare un bo' gia' istantiato, se tanto poi *)
+(*CSC: ci ripasso sopra apply_subst!!! *)
+(*CSC: Inoltre, potrebbe essere questa funzione ad applicare apply_subst a *)
+(*CSC: newmetasenv!!! *)
+let refine_meta_with_brand_new_metasenv meta term apply_subst_replacing
+ newmetasenv
+=