bugfix: handle trigger annotations for nested quantifiers

[tjhance]

This fixes the second item in #717

Namely, it allows this to pass by not adding f(x) as a trigger on the inner quantifier:

        spec fn f(x: int) -> bool;
        spec fn g(x: int) -> bool;

        proof fn test() {
            // trigger for outer quantifier should be f(x)
            // trigger for inner quantifier should be g(y) (and NOT include f(x))
            assume(forall |x: int|
              forall |y: int|
                #[trigger] f(x) && #[trigger] g(y));

            let t = f(3);
            let u = g(4);
            assert(f(3) && g(4));
        }

As an incidental fix, we also fix a small issue with the trigger-collector not recognizing uses of const generic params. You can now write:

        pub open spec fn stuff(t: int) -> bool { true }

        #[verifier::external_body]
        pub broadcast proof fn broadcaster<const X: u8>()                                               
            ensures #[trigger] stuff(X as int) ==> 0 <= X < 255                                         
        {           
        }