表記の扱いが異なることに気付きました。たとえば、<は通常の定義の単なる表記でありunfold "<"、次の例のように機能します。
Theorem a : 4 < 5.
Proof.
unfold "<".
ただし、次の例のように<=、表記法が型に関連付けられておりle、何らかの理由unfold "<="で機能しません。
Theorem a : 4 <= 5
Proof.
unfold "<=".
で失敗しUnable to interpret "<=" as a referenceます。
ltac コマンドで変換できます4 <= 5か?le 4 5