- theory of llor now includes (long awaited) non-recursive alternative definition

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / substitution / llpx_sn_tc.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/llpx_sn_tc.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/llpx_sn_tc.ma
index d22e0906987d1c87674d978a62b967e2c410c425..1ab9a7984386e6c9980145c2d96c9f8f7c14985e 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/substitution/llpx_sn_tc.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/llpx_sn_tc.ma
@@ -18,8 +18,8 @@ include "basic_2/substitution/llpx_sn_ldrop.ma".
 
 (* Properties about transitive closure **************************************)
 
-lemma llpx_sn_TC_pair_dx: ∀R. (∀I,L. reflexive … (R I L)) →
-                          ∀I,L,V1,V2,T. LTC … (R I) L V1 V2 →
+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).
 #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/