X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2A%2Fmultiple%2Fllpx_sn_tc.ma;h=344533743abf81b700ad1568bb4944f4ad57086d;hb=1fd63df4c77f5c24024769432ea8492748b4ac79;hp=97e0580396b4f5cf9a29a82f4d1ef89ad2156876;hpb=277fc8ff21ce3dbd6893b1994c55cf5c06a98355;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2A/multiple/llpx_sn_tc.ma b/matita/matita/contribs/lambdadelta/basic_2A/multiple/llpx_sn_tc.ma
index 97e058039..344533743 100644
--- a/matita/matita/contribs/lambdadelta/basic_2A/multiple/llpx_sn_tc.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2A/multiple/llpx_sn_tc.ma
@@ -19,8 +19,8 @@ include "basic_2A/multiple/llpx_sn_drop.ma".
 (* Properties about transitive closure **************************************)
 
 lemma llpx_sn_TC_pair_dx: ∀R. (∀L. reflexive … (R L)) →
-                          ∀I,L,V1,V2,T. LTC … R L V1 V2 →
-                          LTC … (llpx_sn R 0) T (L.ⓑ{I}V1) (L.ⓑ{I}V2).
+                          ∀I,L,V1,V2,T. CTC … R L V1 V2 →
+                          CTC … (llpx_sn R 0) T (L.ⓑ{I}V1) (L.ⓑ{I}V2).
 #R #HR #I #L #V1 #V2 #T #H @(TC_star_ind … V2 H) -V2
 /4 width=9 by llpx_sn_bind_repl_O, llpx_sn_refl, step, inj/
 qed.