val simpl_tac: pattern:ProofEngineTypes.pattern -> ProofEngineTypes.tactic
val reduce_tac: pattern:ProofEngineTypes.pattern -> ProofEngineTypes.tactic
val whd_tac: pattern:ProofEngineTypes.pattern -> ProofEngineTypes.tactic
val normalize_tac: pattern:ProofEngineTypes.pattern -> ProofEngineTypes.tactic
val simpl_tac: pattern:ProofEngineTypes.pattern -> ProofEngineTypes.tactic
val reduce_tac: pattern:ProofEngineTypes.pattern -> ProofEngineTypes.tactic
val whd_tac: pattern:ProofEngineTypes.pattern -> ProofEngineTypes.tactic
val normalize_tac: pattern:ProofEngineTypes.pattern -> ProofEngineTypes.tactic