From a49f76378fe4aee5b14c71295e11196aa570c583 Mon Sep 17 00:00:00 2001
From: gabrielhdt <gabrielhondet@gmail.com>
Date: Wed, 22 Apr 2020 12:03:58 +0200
Subject: [PATCH] eqind, newline

---
 encodings/bool_hol.lp |  2 +-
 prelude/logic.lp      | 10 ++++++++--
 2 files changed, 9 insertions(+), 3 deletions(-)

diff --git a/encodings/bool_hol.lp b/encodings/bool_hol.lp
index 03996ce..586c9e1 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 ac96dc8..ae3b846 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
 //
-- 
GitLab