val identity_relocation_list_for_metavariable :
  'a option list -> Cic.term option list
val new_meta : proof:('a * (int * 'b * 'c) list * 'd * 'e) option -> int
val subst_meta_in_proof :
  ProofEngineTypes.proof ->
  int -> Cic.term -> Cic.metasenv ->
  ProofEngineTypes.proof * Cic.metasenv
val subst_meta_and_metasenv_in_proof :
  ProofEngineTypes.proof ->
  int -> (Cic.term -> Cic.term) -> Cic.metasenv ->
  ProofEngineTypes.proof * Cic.metasenv