How do I write the Lark grammar to extend logical statements by bounded second-order quantifiers?

Question

I have been developing a Lark grammar to handle statements in the following format:

R is reflexive & S is reflexive -> R | S is reflexive

The current version assumes that all binary relations (R and S, in this example), along with the set A (on which the relations are defined), are provided by the user. The input looks like this:

A = {1,2,3}
R = BinaryRelation({(1,1)}, A, A)
S = BinaryRelation({(2,2),(3,3)}, A, A)

How can I extend the functionality and Lark grammar to parse bounded universal quantifiers? The statements would then look like this:

∀R<AxA ∀S<AxA (R is reflexive & S is reflexive -> R | S is reflexive)

where the input will only be the set A, for example:

A = {1,2,3}

Here is my current version of Lark grammar:

RELATION: CNAME
%import common.CNAME
?logical_implication: logical_and_or
        | logical_implication "->" logical_and_or  -> implication
?logical_and_or: predicate
        | logical_and_or "and" predicate  -> conjunction
        | logical_and_or "or"  predicate  -> disjunction
?predicate: special_operator
        | predicate "="  special_operator  -> equal
        | predicate "!="  special_operator  -> not_equal
        | predicate ">"   special_operator  -> greater_than
        | predicate "<"   special_operator  -> lower_than
        | predicate ">="  special_operator  -> greater_equal
        | predicate "<="  special_operator  -> lower_equal                   
?special_operator: properties
        | "not" predicate      -> negation
        | expression "is" properties     -> is
        | expression "is not" properties -> is_not
?properties: expression    
        | "total_order"   -> total_order
        | "transitive"    -> transitive
        | "reflexive"     -> reflexive
        | "symmetric"     -> symmetric
        | "asymmetric"    -> asymmetric
        | "antisymmetric" -> antisymmetric
        | "irreflexive"   -> irreflexive
?expression: literal
        | "\i{" expression "}"  -> inverse
        | expression "\o" literal   -> composition
        | expression "&" literal   -> intersection
        | expression "|" literal   -> union
        | expression "-" literal   -> difference
        | expression "^" literal   -> symmetric_difference
        | "\c{" expression "}"  -> complement
?literal: "("logical_implication")"
        | RELATION
%import common.WS
%ignore WS