let fresh_meta = ProofEngineHelpers.new_meta proof in
let irl =
ProofEngineHelpers.identity_relocation_list_for_metavariable context in
let fresh_meta = ProofEngineHelpers.new_meta proof in
let irl =
ProofEngineHelpers.identity_relocation_list_for_metavariable context in
let fresh_meta = ProofEngineHelpers.new_meta proof in
let irl =
ProofEngineHelpers.identity_relocation_list_for_metavariable context in
let fresh_meta = ProofEngineHelpers.new_meta proof in
let irl =
ProofEngineHelpers.identity_relocation_list_for_metavariable context in