(* clean_up_meta take a metasenv and a term and make every local context
of each occurrence of a metavariable consistent with its canonical context,
with respect to the hidden hipothesis *)
(* clean_up_meta take a metasenv and a term and make every local context
of each occurrence of a metavariable consistent with its canonical context,
with respect to the hidden hipothesis *)