val replace_with_rel_1_from :
equality:(Cic.term -> Cic.term -> bool) ->
what:Cic.term list -> int -> Cic.term -> Cic.term
-val reduce : Cic.context -> Cic.term -> Cic.term
val simpl : Cic.context -> Cic.term -> Cic.term
val unfold : ?what:Cic.term -> Cic.context -> Cic.term -> Cic.term