Lines Matching refs:prefix
172 |- !u E. OBS_CONGR (prefix u (prefix tau E)) (prefix u E) *)192 |- !E. OBS_CONGR (sum E (prefix tau E)) (prefix tau E)211 OBS_CONGR (sum (prefix u (sum E (prefix tau E'))) (prefix u E'))212 (prefix u (sum E (prefix tau E')))