{-# 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