in
let fresh_meta = ProofEngineHelpers.new_meta_of_proof proof in
let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in
in
let fresh_meta = ProofEngineHelpers.new_meta_of_proof proof in
let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in