Могут ли логические `и` быть заменены оператором if и при этом иметь такую ​​же семантику большого шага?

Question

В системе, приведенной ниже, можно ли заменить все подстановки and t1 t2 в некотором операторе T (где T with v) на if t1 then t2 else false и все еще получить тот же результат, то есть T ⇓ v?

Answer 1

Нет, потому что and err false уменьшается до false, но if err then false else false застревает.