Element versus Subgroup

Dear all,

If I do

        reserve G for Group;
        reserve H for Subgroup of G;
        reserve h for Element of H;

(like in GROUP_2, for example), I don't think I can make

        h qua Element of G

work.  I think one would have to redefine the type of a
field in a structure, or something like that, and I don't
see how to do that.

So are these thoughts correct?

And if one would do structures in the Lee/Rudnicki way,
would this be different?

Freek