Induction: Adds solutions to beg_nat_refl and plus_swap'.