1 Goal "!xs. linInfixList t xs = infixList t @ xs";
2 by(induct_tac "t" 1);
3 by(Simp_tac 1);
4 by(Asm_simp_tac 1);