val symmetry : ProofEngineTypes.tactic
val transitivity : term:Cic.term -> ProofEngineTypes.tactic
val unfold :
- ?what:Cic.term ->
+ Cic.term option ->
pattern:ProofEngineTypes.pattern -> ProofEngineTypes.tactic
val whd : pattern:ProofEngineTypes.pattern -> ProofEngineTypes.tactic