by(induct_tac "xs" 1);