let clear = ProofEngineStructuralRules.clear
let clearbody = ProofEngineStructuralRules.clearbody
let compare = DiscriminationTactics.compare_tac
let clear = ProofEngineStructuralRules.clear
let clearbody = ProofEngineStructuralRules.clearbody
let compare = DiscriminationTactics.compare_tac