diff --git a/adlib/booleans.lp b/adlib/booleans.lp
index 528c4cc11a1f50e0ee9a3a56559e45f4f5c27abd..71bb5c811b9e7566c8cfb019dd9991aaee05b61a 100644
--- a/adlib/booleans.lp
+++ b/adlib/booleans.lp
@@ -1,6 +1,7 @@
 require open
   personoj.encodings.lhol
   personoj.encodings.pvs_cert
+  personoj.encodings.booleans
 
 definition false ≔ forall {bool} (λx, x)
 definition true ≔ impd {false} (λ_, false)
@@ -19,8 +20,6 @@ set infix 7 "⇔" ≔ biff
 
 definition when P Q ≔ imp Q P
 
-set builtin "bot" ≔ false
-set builtin "top" ≔ true
 set builtin "imp" ≔ imp
 set builtin "not" ≔ bnot
 set builtin "and" ≔ band
diff --git a/encodings/booleans.lp b/encodings/booleans.lp
new file mode 100644
index 0000000000000000000000000000000000000000..9a300d1a96895243573e85562b70d008137b75e8
--- /dev/null
+++ b/encodings/booleans.lp
@@ -0,0 +1,8 @@
+require open personoj.encodings.lhol
+  personoj.encodings.pvs_cert
+
+definition false ≔ forall {bool} (λx, x)
+definition true ≔ impd {false} (λ_, false)
+
+set builtin "bot" ≔ false
+set builtin "top" ≔ true
diff --git a/encodings/if.lp b/encodings/if.lp
index f625e1f6a37e1cc1f88b728234b8eda50908418b..02c8556a3ac6b23040e3b47a27ef96524bc1dd02 100644
--- a/encodings/if.lp
+++ b/encodings/if.lp
@@ -1,6 +1,15 @@
 require open personoj.encodings.lhol
   personoj.encodings.pvs_cert
-  personoj.encodings.subtype
+  personoj.encodings.booleans
+require personoj.encodings.deferred as Deferred
+require open personoj.encodings.subtype //FIXME: why must it be the last import?
 
 symbol if {U: Set} {V: Set} (S: Set)
 : ε (U ⊑ S) ⇒ ε (V ⊑ S) ⇒ Bool ⇒ η U ⇒ η V ⇒ η S
+
+symbol lif {U: Set} {V: Set} (S: Set)
+: ε (U ⊑ S) ⇒ ε (V ⊑ S) ⇒ Bool ⇒ Deferred.t U ⇒ Deferred.t V ⇒ η S
+
+// lazy if
+rule lif _ &pr _ true &t _ → ↑ &pr (Deferred.unquote &t)
+rule lif _ _ &pr false _ &f → ↑ &pr (Deferred.unquote &f)
diff --git a/encodings/subtype.lp b/encodings/subtype.lp
index 6f27ed9440f987a282b88f619408c34729fb8614..4ed85f1205c18a5e4ef839ea5561a089e9a83b45 100644
--- a/encodings/subtype.lp
+++ b/encodings/subtype.lp
@@ -1,6 +1,8 @@
 require open personoj.encodings.lhol
 require open personoj.encodings.pvs_cert
 
+set declared "↑"
+
 symbol subtype : Set ⇒ Set ⇒ Bool
 set infix left 6 "⊑" ≔ subtype
 
@@ -14,6 +16,7 @@ symbol S_Darr (d: Set) (r1: η d ⇒ Set) (r2: η d ⇒ Set)
 : ε (forall (λx, (r1 x) ⊑ (r2 x))) ⇒ ε ((arrd r1) ⊑ (arrd r2))
 
 symbol upcast {A: Set} {B: Set}: ε (A ⊑ B) ⇒ η A ⇒ η B
+definition ↑ {A} {B} ≔ upcast {A} {B}
 
 symbol root: Set ⇒ Set
 rule root (psub {&T} _) → root &T
diff --git a/sandbox/quote.lp b/sandbox/quote.lp
index 5f0466fc756f32e206681a10692444ad26c154ae..0cf4195973201ccc5b745f41d571e5b2347daf76 100644
--- a/sandbox/quote.lp
+++ b/sandbox/quote.lp
@@ -17,3 +17,5 @@ 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)
+
+symbol lor: Deferred.t bool ⇒ Deferred.t bool ⇒ Bool