tactic.itauto.proof source