rzk-0.9.0: test/typecheck/cases/ill-tope-not-satisfied-rec-or-open-singleton.rzk

#lang rzk-1

-- Single-branch `recOR` on unrestricted `t : 2`: `contextEntailsUnion` requires `⊤` to entail
-- `t ≡ 0₂ ∨ ⊥`, which fails (`contextEntailsUnion` after `recOR`).

#define u : U := Unit -> Unit

#define openSingleton (t : 2) : U
  := recOR( t === 0_2 |-> u )