diff --git a/encodings/bool_hol.lp b/encodings/bool_hol.lp
new file mode 100644
index 0000000000000000000000000000000000000000..ac2f5c121fc93b5263e88d2f918ebb40b230f73f
--- /dev/null
+++ b/encodings/bool_hol.lp
@@ -0,0 +1,27 @@
+// Definition based on implication
+require open personoj.encodings.lhol
+require open personoj.encodings.pvs_cert
+
+definition false ≔ forall {bool} (λx, x)
+definition true ≔ impd {false} (λ_, false)
+
+definition not P ≔ impd {P} (λ_, false)
+set prefix 5 "¬" ≔ not
+
+definition imp P Q ≔ impd {P} Q
+set infix 2 "⊃" ≔ imp
+
+definition {|and|} P Q ≔ ¬ (P ⊃ (λh, ¬ (Q h)))
+set infix 4 "∧" ≔ {|and|}
+definition or P Q ≔ (¬ P) ⊃ Q
+set infix 3 "∨" ≔ or
+
+set builtin "bot" ≔ false
+set builtin "top" ≔ true
+set builtin "not" ≔ not
+set builtin "imp" ≔ imp
+set builtin "and" ≔ {|and|}
+set builtin "or"  ≔ or
+
+symbol if {s: Set} p: (ε p ⇒ η s) ⇒ (ε (¬ p) ⇒ η s) ⇒ η s
+rule if {bool} &p &then &else → (&p ⊃ &then) ⊃ (λ_, ¬ &p ⊃ &else)
diff --git a/encodings/bool_pvs.lp b/encodings/bool_pvs.lp
new file mode 100644
index 0000000000000000000000000000000000000000..00941455718072b284cae6d81e5ba88bd3eaaab3
--- /dev/null
+++ b/encodings/bool_pvs.lp
@@ -0,0 +1,31 @@
+// Close to PVS logic system: native equality,
+// true, false, and if
+require open personoj.encodings.lhol
+require open personoj.encodings.pvs_cert
+
+definition false ≔ forall {bool} (λx, x)
+definition true ≔ impd {false} (λ_, false)
+
+symbol eq {s: Set}: η s ⇒ η s ⇒ η bool
+set infix left 6 "=" ≔ eq
+
+definition not p ≔ eq {bool} p false
+set prefix 5 "¬" ≔ not
+
+constant symbol if {s: Set} p: (ε p ⇒ η s) ⇒ (ε (¬ p) ⇒ η s) ⇒ η s
+rule ε (if &p &then &else)
+   → (∀h: ε &p, ε (&then h)) ⇒ ∀h: ε (¬ &p), ε (&else h)
+
+definition {|and|} p q ≔ if {bool} p q (λ_, false)
+definition or p q ≔ if {bool} p (λ_, true) q
+definition imp p q ≔ if {bool} p q (λ_, true)
+set infix left 4 "∧" ≔ {|and|}
+set infix left 3 "∨" ≔ or
+set infix left 2 "⊃" ≔ imp
+
+set builtin "bot" ≔ false
+set builtin "top" ≔ true
+set builtin "not" ≔ not
+set builtin "imp" ≔ imp
+set builtin "and" ≔ {|and|}
+set builtin "or"  ≔ or
diff --git a/encodings/boolops_if.lp b/encodings/boolops_if.lp
index e9faca794d07a8d405539c0fa62fde98f0a5670c..ba1b39b3860703537f91a265b621f1d65c21d30d 100644
--- a/encodings/boolops_if.lp
+++ b/encodings/boolops_if.lp
@@ -1,9 +1,8 @@
 // Boolean operators defined from if.
-require open
-  personoj.encodings.lhol
-  personoj.encodings.pvs_cert
-  personoj.encodings.booleans
-  personoj.encodings.if
+require open personoj.encodings.lhol
+require open  personoj.encodings.pvs_cert
+require open  personoj.encodings.booleans
+require open  personoj.encodings.if
 
 // Definition of logical connectors with if3
 definition band p q ≔ if {bool} p q (λ_, false)
diff --git a/sandbox/boolops_if.lp b/sandbox/boolops_if.lp
new file mode 100644
index 0000000000000000000000000000000000000000..735934d90859da7e3f503e35bf6895a8a96c6d98
--- /dev/null
+++ b/sandbox/boolops_if.lp
@@ -0,0 +1,9 @@
+require open personoj.encodings.lhol
+require open personoj.encodings.pvs_cert
+require open personoj.encodings.bool_pvs
+
+theorem trivial (P: η bool): ε (P ⊃ (λ_, P))
+proof
+  assume P
+  refine λ_ _ f, f
+qed