diff --git a/encodings/bool_hol.lp b/encodings/bool_hol.lp
index 03996ce5818dae04cbbc8ac900170302445b7545..586c9e13b37da5716f96fa2a7d45b28905d231f2 100644
--- a/encodings/bool_hol.lp
+++ b/encodings/bool_hol.lp
@@ -30,4 +30,4 @@ symbol eq {s: Set}: η s → η s → η bool
 set infix 2 "=" ≔ eq
 set builtin "eq" ≔ eq // FIXME emacs indentation
 
-rule ε ($x = $y) ↪ ΠP: η (_ ~> bool), ε (P $x) → ε (P $y)
+rule ε ($x = $y) ↪ Πp: η (_ ~> bool), ε (p $x) → ε (p $y)
diff --git a/prelude/logic.lp b/prelude/logic.lp
index ac96dc8363a15506a4f3856ef57f2091b90b34ef..ae3b846c235e14f76f1a25abc571e1c329ae4816 100644
--- a/prelude/logic.lp
+++ b/prelude/logic.lp
@@ -9,7 +9,6 @@ require open personoj.encodings.prenex
 //
 // Equalities
 //
-// in [adlib.cert_f.bootstrap]
 
 //
 // Notequal
@@ -82,7 +81,6 @@ definition SETOF ≔ pred
 // equality_props
 //
 
-set debug +ui
 constant
 symbol If_true
      : ε (∀B
@@ -118,6 +116,14 @@ constant
 symbol symmetry_of_equals
      : ε (∀B (λt, forall (λx: η t, (forall (λy: η t, (x = y) ⊃ (λ_, y = x))))))
 
+// Not in prelude!
+theorem eqind {t} x y: ε (x = y) → Πp: η t → Bool, ε (p y) → ε (p x)
+proof
+  assume t x y heq
+  apply symmetry_of_equals t x y heq
+qed
+set builtin "eqind" ≔ eqind
+
 //
 // if_props
 //