by(induct_tac "xs" 1); by(Auto_tac);