ill-tope-not-satisfied-app-shape.rzk

#lang rzk-1

-- Applying a function typed on a strict shape requires the corresponding tope in the
-- local context (`contextEntails` on the guard after substituting the argument).

#define app (f : (t : 2 | t === 0_2) -> U) (x : 2) : U
  := f x