val alpha_equivalence: Cic.term -> Cic.term -> bool
val replace :
- equality:(Cic.term -> 'a -> bool) ->
+ equality:('a -> Cic.term -> bool) ->
what:'a list -> with_what:Cic.term list -> where:Cic.term -> Cic.term
val replace_lifting :
equality:(Cic.term -> Cic.term -> bool) ->
what:Cic.term list -> with_what:Cic.term list -> where: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