(* Replaces "textually" in "where" every term in "what" with the corresponding
term in "with_what". The terms in "what" ARE NOT lifted when binders are
crossed. The terms in "with_what" ARE NOT lifted when binders are crossed.
(* Replaces "textually" in "where" every term in "what" with the corresponding
term in "with_what". The terms in "what" ARE NOT lifted when binders are
crossed. The terms in "with_what" ARE NOT lifted when binders are crossed.
what:Cic.term list -> with_what:Cic.term list -> where:Cic.term -> Cic.term
(* Replaces in "where" every term in "what" with the corresponding
what:Cic.term list -> with_what:Cic.term list -> where:Cic.term -> Cic.term
(* Replaces in "where" every term in "what" with the corresponding
val replace_with_rel_1_from :
equality:(Cic.term -> Cic.term -> bool) ->
what:Cic.term list -> int -> Cic.term -> Cic.term
val replace_with_rel_1_from :
equality:(Cic.term -> Cic.term -> bool) ->
what:Cic.term list -> int -> Cic.term -> Cic.term
val simpl : Cic.context -> Cic.term -> Cic.term
val unfold : ?what:Cic.term -> 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