diff --git a/encodings/lazy.lp b/encodings/deferred.lp
similarity index 52%
rename from encodings/lazy.lp
rename to encodings/deferred.lp
index c350a8946b8d26a89e54ab56a8ab5e64c6b33271..4107912032b219c7b4890f7a5e296cd335af278a 100644
--- a/encodings/lazy.lp
+++ b/encodings/deferred.lp
@@ -1,19 +1,20 @@
+// Encoding of deferred terms. It ought to be used by lazy operators such as IF
+// or boolean operators
 require open
   personoj.encodings.lhol
   personoj.encodings.pvs_cert
 
-constant symbol delayed: Set ⇒ TYPE
-constant symbol quote {T: Set}: η T ⇒ delayed T
+constant symbol t: Set ⇒ TYPE
+constant symbol quote {T: Set}: η T ⇒ t T
 
 // Application at sort type
 symbol sapp: Set ⇒ Set ⇒ Set
 rule sapp (&T ~> &S) &T → &T
 
 // Quoted terms application
-constant symbol app {T: Set} {S: Set}
-: delayed T ⇒ delayed S ⇒ delayed (sapp T S)
+constant symbol app {T: Set} {S: Set}: t T ⇒ t S ⇒ t (sapp T S)
 
 // Unquote terms
-symbol unquote {T: Set}: delayed T ⇒ η T
+symbol unquote {T: Set}: t T ⇒ η T
 rule unquote (quote &x) → &x
 rule unquote {&S} (app {&T ~> &S} {&T} &t &u) → (unquote &t) (unquote &u)
diff --git a/sandbox/quote.lp b/sandbox/quote.lp
index e6f91de69a51d8315f2aa4cbd2547795bde6a546..5f0466fc756f32e206681a10692444ad26c154ae 100644
--- a/sandbox/quote.lp
+++ b/sandbox/quote.lp
@@ -1,17 +1,19 @@
 require open
   personoj.encodings.lhol
   personoj.encodings.pvs_cert
-require personoj.encodings.lazy as L
+require personoj.encodings.deferred as Deferred
 
-symbol T: Set
+constant symbol T: Set
 symbol t: η T
 symbol f: η (T ~> T)
-symbol S: Set
+constant symbol S: Set
 symbol s: η S
 
 set flag "print_implicits" on
-definition qu_ko ≔ L.app (L.quote f) (L.quote s)
-compute L.unquote qu_ko
+definition qu_ko ≔ Deferred.app (Deferred.quote f) (Deferred.quote s)
+compute Deferred.unquote qu_ko
 
-definition qu_ok ≔ L.app (L.quote f) (L.quote t)
-compute L.unquote qu_ok
+definition qu_ok ≔ Deferred.app (Deferred.quote f) (Deferred.quote t)
+compute Deferred.unquote qu_ok
+
+compute Deferred.quote {T ~> T} (λx:η T, f x)