Working with lambda abstraction capturing binding effects

Hi,

I am trying to get this sorted out.
I would like to encode an object level logic following the conventions
of Programming with Higher-Order Logic.

% categories
kind term type.
kind form type.

% connectives
type ==> form -> form -> form.
type &&    form -> form -> form.

infixl && 5.
infixr ==> 3.

% quantifiers
type all term -> form -> form.
type some term -> form -> form.

% predicate symbols
p: term -> form.
q : term -> form.

% term constant symbols
a: term.
f: term -> term.

To introduce some object formulae as knowledge I use a predicate frm
    type frm form -> o.

such that I know for instance:
    frm (p a ==> q a).
    frm (all x\ all y\ p x && r y ==> q y).

Now I would like to uniformally treat qantified and ground formulae in
reasoning about them; Just assume for the sake of the example I would
like to unify all formuale that imply q a.
Naively I would try something like
    frm F (X ==> q a).

Is there an elegant solution to this?

Thanks for your support.

Best,
Jakob