val whd_tac: pattern:ProofEngineTypes.lazy_pattern -> ProofEngineTypes.tactic
val normalize_tac: pattern:ProofEngineTypes.lazy_pattern -> ProofEngineTypes.tactic
val head_beta_reduce_tac: ?delta:bool -> ?upto:int -> pattern:ProofEngineTypes.lazy_pattern -> ProofEngineTypes.tactic
val whd_tac: pattern:ProofEngineTypes.lazy_pattern -> ProofEngineTypes.tactic
val normalize_tac: pattern:ProofEngineTypes.lazy_pattern -> ProofEngineTypes.tactic
val head_beta_reduce_tac: ?delta:bool -> ?upto:int -> pattern:ProofEngineTypes.lazy_pattern -> ProofEngineTypes.tactic