for A being QC-alphabet
for F, G being Element of QC-WFF A st F is_subformula_of G & len (@ F) = len (@ G) holds
F = G by QC_LANG2:54, QC_LANG2:def 21;