X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Fbasics%2Fstar.ma;h=00a23b633a206017c0fce733f605a111adc681c0;hb=b08fbe87149ae7c2e14dfd7485dbf50d6e7dbfe6;hp=6592592aa6f092861531fa9e95e97fa841559e06;hpb=784a534f6d969a261f45396307d0ef30f7fb2be2;p=helm.git

diff --git a/matita/matita/lib/basics/star.ma b/matita/matita/lib/basics/star.ma
index 6592592aa..00a23b633 100644
--- 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.