Если rsltc ругается на pre у аксиомы

Согласно синтаксису RSL, который поддерживает rsltc (RSL Type Checker), см. http://www.iist.unu.edu/www/newrh/III/3/1/docs/rsltc/user_guide/syntax.zip , pre у аксиомы можно писать только в том случае, если аксиома имеет вид all ... :- expr1 is expr2 . Если подкванторное выражение более сложное, надо либо его преобразовать к эквивалентности (это желательный способ избавления от этой проблемы), либо вместо pre записать импликацию (нежелательный способ решения этой проблемы).