let assumption = VariousTactics.assumption_tac
let auto = AutoTactic.auto_tac
let change = ReductionTactics.change_tac
let clear = ProofEngineStructuralRules.clear
let clearbody = ProofEngineStructuralRules.clearbody
let assumption = VariousTactics.assumption_tac
let auto = AutoTactic.auto_tac
let change = ReductionTactics.change_tac
let clear = ProofEngineStructuralRules.clear
let clearbody = ProofEngineStructuralRules.clearbody