Add type guards for quantification over functions returning finite types

It is obvious that I need to do it on skolemised variables. This is
trying to prove filter p/++ homomorphism without induction:

cnf(x, axiom,
    f_filter(a_p,'f_++'(a_xs,a_ys)) != 'f_++'(f_filter(a_p,a_xs)
                                             ,f_filter(a_p,a_ys))).
cnf(x, axiom, type(app(a_p,X),f_Bool)).

However, do I need to have the type guards when adding these as lemmas?
Like here:

fof('Lemma{filter p xs++filter p ys == filter p (xs++ys)}', lemma,
    ! [X_0,Y,Z] :
        ((! [X] : type(app(X_0,X),f_Bool))
          => 'f_++'(f_filter(X_0,Y),f_filter(X_0,Z)) =
                    f_filter(X_0,'f_++'(Y,Z)))).

This is not obvious for me why it should be required.