let newmeta = ProofEngineHelpers.new_meta_of_proof ~proof in
let ok_types ty menv =
List.for_all (fun (_, _, mt) -> mt = ty) menv
let newmeta = ProofEngineHelpers.new_meta_of_proof ~proof in
let ok_types ty menv =
List.for_all (fun (_, _, mt) -> mt = ty) menv