for p, q being Element of HP-WFF
for t being FinSequence st p = q ^ t holds
p = q