(Cic.name option) list -> goal_proof -> proof -> int -> unit
val pp_proofterm: Cic.term -> string
+
+val mk_eq_ind :
+ UriManager.uri ->
+ Cic.term ->
+ Cic.term ->
+ Cic.term ->
+ Cic.term ->
+ Cic.term ->
+ Cic.term ->
+ Cic.term
val mk_equality :
equality_bag -> int * proof *