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

diff --git a/matita/matita/contribs/lambdadelta/ground_2/lib/relations.ma b/matita/matita/contribs/lambdadelta/ground_2/lib/relations.ma
index 3f5c3b409..e62b1fcda 100644
--- a/matita/matita/contribs/lambdadelta/ground_2/lib/relations.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/lib/relations.ma
@@ -94,3 +94,12 @@ lemma NF_to_SN_sn: ∀A,R,S,a. NF_sn A R S a → SN_sn A R S a.
 @SN_sn_intro #a1 #HRa12 #HSa12
 elim HSa12 -HSa12 /2 width=1 by/
 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.