for Q being Girard-Quantale
for a1, a2, b1, b2 being Element of Q st a1 [= b1 & a2 [= b2 holds
a1 delta a2 [= b1 delta b2