*)
val equality_of_term: Cic.term -> Cic.term -> equality
+(**
+ Re-builds the term corresponding to this equality
+*)
+val term_of_equality: equality -> Cic.term
+
val term_is_equality: Cic.term -> bool
(** tests a sort of alpha-convertibility between the two terms, but on the