{-# OPTIONS --without-K --safe --no-sized-types --no-guardedness --no-subtyping #-} module Agda.Builtin.Strict where open import Agda.Builtin.Equality primitive primForce : ∀ {a b} {A : Set a} {B : A → Set b} (x : A) → (∀ x → B x) → B x primForceLemma : ∀ {a b} {A : Set a} {B : A → Set b} (x : A) (f : ∀ x → B x) → primForce x f ≡ f x