(* SHIFT OF A CLOSURE *******************************************************)
let rec shift L T on L ≝ match L with
[ LAtom ⇒ T
(* SHIFT OF A CLOSURE *******************************************************)
let rec shift L T on L ≝ match L with
[ LAtom ⇒ T