X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground_2%2Flib%2Fstar.ma;h=cc8a4318c61628d6882fa9b8ea3ebd1edfff4f4f;hb=5ad776e509cd35fa003292e8bf2ed8f31d2c0a4b;hp=fdf2ae5a4e648bfcac7fe3ba5a3c6ad37889587f;hpb=a961853f4bb6f26c4cc8ca9babad0de0e6c6d1ff;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/ground_2/lib/star.ma b/matita/matita/contribs/lambdadelta/ground_2/lib/star.ma
index fdf2ae5a4..cc8a4318c 100644
--- a/matita/matita/contribs/lambdadelta/ground_2/lib/star.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/lib/star.ma
@@ -192,13 +192,6 @@ qed-.
 
 (* Relations on unboxed triples *********************************************)
 
-definition tri_RC: ∀A,B,C. tri_relation A B C → tri_relation A B C ≝
-                   λA,B,C,R,a1,b1,c1,a2,b2,c2. R … a1 b1 c1 a2 b2 c2 ∨
-                   ∧∧ a1 = a2 & b1 = b2 & c1 = c2.
-
-lemma tri_RC_reflexive: ∀A,B,C,R. tri_reflexive A B C (tri_RC … R).
-/3 width=1 by and3_intro, or_intror/ qed.
-
 definition tri_star: ∀A,B,C,R. tri_relation A B C ≝
                      λA,B,C,R. tri_RC A B C (tri_TC … R).