support for nat-labeled reflexive and transitive closure added to lambdadelta

[helm.git] / matita / matita / lib / basics / star.ma

diff --git a/matita/matita/lib/basics/star.ma b/matita/matita/lib/basics/star.ma
index 6592592aa6f092861531fa9e95e97fa841559e06..00a23b633a206017c0fce733f605a111adc681c0 100644 (file)
--- a/matita/matita/lib/basics/star.ma
+++ b/matita/matita/lib/basics/star.ma
@@ -258,9 +258,6 @@ lemma TC_star_ind_dx: ∀A,R. reflexive A R →
 @(TC_ind_dx … P ? H … Ha12) /3 width=4/
 qed-.
 
-definition Conf3: ∀A,B. relation2 A B → relation A → Prop ≝ λA,B,S,R.
-                  ∀b,a1. S a1 b → ∀a2. R a1 a2 → S a2 b.
-
 lemma TC_Conf3: ∀A,B,S,R. Conf3 A B S R → Conf3 A B S (TC … R).
 #A #B #S #R #HSR #b #a1 #Ha1 #a2 #H elim H -a2 /2 width=3/
 qed.