tactic.by_contradiction source