1 Goal "subst Var t = (t ::('a,'b)term) & \
2 \ substs Var ts = (ts::('a,'b)term list)";
3 by(mutual_induct_tac ["t", "ts"] 1);
4 by(Auto_tac);