basic_induction, double_plus, beq_nat_refl