Abbreviations

Let , be distinct variables. Abbreviate

choose  in U
     choose  in U   
           
     endchoose
endchoose

to

choose ,  in U
           
endchoose

In a similar way define abbreviation

choose , ...,  in U
           
endchoose