diff --git a/encodings/lazy.lp b/encodings/lazy.lp
index 80b424be153a1f897a6c0447c0e0326f85e56d11..c350a8946b8d26a89e54ab56a8ab5e64c6b33271 100644
--- a/encodings/lazy.lp
+++ b/encodings/lazy.lp
@@ -5,12 +5,15 @@ require open
 constant symbol delayed: Set ⇒ TYPE
 constant symbol quote {T: Set}: η T ⇒ delayed T
 
-constant symbol s_app: Set ⇒ Set ⇒ Set
+// 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 (s_app T S)
+: delayed T ⇒ delayed S ⇒ delayed (sapp T S)
 
+// Unquote terms
 symbol unquote {T: Set}: delayed 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
new file mode 100644
index 0000000000000000000000000000000000000000..e6f91de69a51d8315f2aa4cbd2547795bde6a546
--- /dev/null
+++ b/sandbox/quote.lp
@@ -0,0 +1,17 @@
+require open
+  personoj.encodings.lhol
+  personoj.encodings.pvs_cert
+require personoj.encodings.lazy as L
+
+symbol T: Set
+symbol t: η T
+symbol f: η (T ~> T)
+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_ok ≔ L.app (L.quote f) (L.quote t)
+compute L.unquote qu_ok