let subst_meta_and_metasenv_in_proof proof meta subst newmetasenv =
let (uri,_,initial_subst,bo,ty, attrs) = proof in
let subst_in = CicMetaSubst.apply_subst subst in
let subst_meta_and_metasenv_in_proof proof meta subst newmetasenv =
let (uri,_,initial_subst,bo,ty, attrs) = proof in
let subst_in = CicMetaSubst.apply_subst subst in