- lambda: some parts commented out, some refactoring

[helm.git] / matita / matita / contribs / lambda / preamble.ma

diff --git a/matita/matita/contribs/lambda/preamble.ma b/matita/matita/contribs/lambda/preamble.ma
index 958f1059a053b90a4f7f0fea0a9c39a8a3c72555..c7c736f2ce1d3cad45775d2568fa537914ca2691 100644 (file)
--- a/matita/matita/contribs/lambda/preamble.ma
+++ b/matita/matita/contribs/lambda/preamble.ma
@@ -28,16 +28,6 @@ notation "⊥"
   non associative with precedence 90
   for @{'false}.
 
-(* relations *)
-
-definition confluent1: ∀A. relation A → predicate A ≝ λA,R,a0.
-                       ∀a1. R a0 a1 → ∀a2. R a0 a2 →
-                       ∃∃a. R a1 a & R a2 a. 
-
-(* Note: confluent1 would be redundant if \Pi-reduction where enabled *)                       
-definition confluent: ∀A. predicate (relation A) ≝ λA,R.
-                      ∀a0. confluent1 … R a0.
-
 (* arithmetics *)
 
 lemma lt_refl_false: ∀n. n < n → ⊥.