diff --git a/encodings/boolops_if.lp b/encodings/boolops_if.lp
new file mode 100644
index 0000000000000000000000000000000000000000..e9faca794d07a8d405539c0fa62fde98f0a5670c
--- /dev/null
+++ b/encodings/boolops_if.lp
@@ -0,0 +1,14 @@
+// Boolean operators defined from if.
+require open
+  personoj.encodings.lhol
+  personoj.encodings.pvs_cert
+  personoj.encodings.booleans
+  personoj.encodings.if
+
+// Definition of logical connectors with if3
+definition band p q ≔ if {bool} p q (λ_, false)
+definition bor p q ≔ if {bool} p (λ_, true) q
+definition imp p q ≔ if {bool} p q (λ_, true)
+set infix left 7 "∧" ≔ band
+set infix left 6 "∧" ≔ bor
+set infix left 5 "⊃" ≔ imp
diff --git a/encodings/boolops_imp.lp b/encodings/boolops_imp.lp
new file mode 100644
index 0000000000000000000000000000000000000000..ed11e1f12a22ccb8963a0a0c4c26a517b9195d78
--- /dev/null
+++ b/encodings/boolops_imp.lp
@@ -0,0 +1,22 @@
+// Boolean operators defined from dependent implication.
+require open
+  personoj.encodings.lhol
+  personoj.encodings.pvs_cert
+  personoj.encodings.booleans
+
+definition imp P Q ≔ impd {P} (λ_, Q)
+set infix 4 "⊃" ≔ imp
+
+definition band P Q ≔ ¬ (P ⊃ (¬ Q))
+definition bor P Q ≔ (¬ P) ⊃ Q
+set infix 6 "∧" ≔ band
+set infix 5 "∨" ≔ bor
+
+definition biff P Q ≔ (P ⊃ Q) ∧ (Q ⊃ P)
+set infix 7 "⇔" ≔ biff
+
+definition when P Q ≔ Q ⊃ P
+
+set builtin "imp" ≔ imp
+set builtin "and" ≔ band
+set builtin "or"  ≔ bor
diff --git a/sandbox/boolops.lp b/sandbox/boolops.lp
new file mode 100644
index 0000000000000000000000000000000000000000..7e3f41580eea0d6a6362b3f473ff6c7e7837f908
--- /dev/null
+++ b/sandbox/boolops.lp
@@ -0,0 +1,25 @@
+// Compute the term [⊥ ⊃ 1 / 0 = 1 / 0]. The principle is that [1/0] is well
+// typed because in the right part of the implication, false is assumed.
+require open personoj.encodings.lhol
+require open personoj.encodings.pvs_cert
+require open personoj.encodings.equality
+require open personoj.encodings.booleans
+
+symbol imp: ∀P: Bool, (ε P ⇒ η bool) ⇒ η bool
+set infix left 6 "⊃" ≔ imp
+
+require personoj.paper.rat as Q
+
+set builtin "0" ≔ Q.Z
+set builtin "+1" ≔ Q.S
+
+theorem zisnotz (h: ε false): ε (Q.{|nznat?|} 0)
+proof
+  assume Hf _
+  refine Hf
+qed
+
+// Computes ⊥ ⊃ (1 / 0) = 1 / 0
+compute false ⊃ (λh,
+                 let ooz ≔ Q.div 1 (pair 0 (zisnotz h)) in
+                 eq ooz ooz)