| SubProof of Cic.term * int * old_proof
and goal_proof = (Utils.pos * int * substitution * Cic.term) list
-
+
+val pp_proof: (Cic.name option) list -> goal_proof -> new_proof -> string
val empty_subst : substitution
val apply_subst : substitution -> Cic.term -> Cic.term
(Cic.term * Cic.term * Cic.term * Utils.comparison) *
Cic.metasenv ->
equality
+
+val mk_tmp_equality :
+ int * (Cic.term * Cic.term * Cic.term * Utils.comparison) * Cic.metasenv ->
+ equality
val open_equality :
equality ->