let fold = ReductionTactics.fold_tac
let fourier = FourierR.fourier_tac
let fwd_simpl = FwdSimplTactic.fwd_simpl_tac
let fold = ReductionTactics.fold_tac
let fourier = FourierR.fourier_tac
let fwd_simpl = FwdSimplTactic.fwd_simpl_tac
let id = Tacticals.id_tac
let intros = PrimitiveTactics.intros_tac
let inversion = Inversion.inversion_tac
let id = Tacticals.id_tac
let intros = PrimitiveTactics.intros_tac
let inversion = Inversion.inversion_tac
let left = IntroductionTactics.left_tac
let letin = PrimitiveTactics.letin_tac
let normalize = ReductionTactics.normalize_tac
let left = IntroductionTactics.left_tac
let letin = PrimitiveTactics.letin_tac
let normalize = ReductionTactics.normalize_tac
let reflexivity = Setoids.setoid_reflexivity_tac
let replace = EqualityTactics.replace_tac
let rewrite = EqualityTactics.rewrite_tac
let reflexivity = Setoids.setoid_reflexivity_tac
let replace = EqualityTactics.replace_tac
let rewrite = EqualityTactics.rewrite_tac
let split = IntroductionTactics.split_tac
let symmetry = EqualityTactics.symmetry_tac
let transitivity = EqualityTactics.transitivity_tac
let split = IntroductionTactics.split_tac
let symmetry = EqualityTactics.symmetry_tac
let transitivity = EqualityTactics.transitivity_tac