TY - RPRT TI - A Novice-Friendly Induction Tactic for Lean AU - Jannis Limperg PY - 2020 UR - https://arxiv.org/abs/2012.08990 ID - 2012.08990 ER -