let cases_intros = PrimitiveTactics.cases_intros_tac
let change = ReductionTactics.change_tac
let clear = ProofEngineStructuralRules.clear
let cases_intros = PrimitiveTactics.cases_intros_tac
let change = ReductionTactics.change_tac
let clear = ProofEngineStructuralRules.clear