val replace :
pattern:ProofEngineTypes.lazy_pattern ->
with_what:Cic.lazy_term -> ProofEngineTypes.tactic
val rewrite :
direction:[ `LeftToRight | `RightToLeft ] ->
pattern:ProofEngineTypes.lazy_pattern ->
val replace :
pattern:ProofEngineTypes.lazy_pattern ->
with_what:Cic.lazy_term -> ProofEngineTypes.tactic
val rewrite :
direction:[ `LeftToRight | `RightToLeft ] ->
pattern:ProofEngineTypes.lazy_pattern ->