module K-Shift-BBC where

open import Logic
open import Naturals
open import JK-Monads
open import J-Shift-BBC


K-∀-shift-bbc : {R : Ω} {A :   Ω}  
-------------

            (∀(n : )  R  A n)                    -- efqs,
            (∀(n : )  K(A n))  K(∀(n : )  A n)  -- shift.

K-∀-shift-bbc efqs φs = J-K(J-∀-shift-bbc n  K-J(efqs n) (φs n)))