the theory of extended multiple substitution for therms is complete

[helm.git] / matita / matita / contribs / lambdadelta / ground_2 / lib / star.ma

diff --git a/matita/matita/contribs/lambdadelta/ground_2/lib/star.ma b/matita/matita/contribs/lambdadelta/ground_2/lib/star.ma
index e5b7887667a0db4a958079569074a45af397ca60..8cfdf349eb25a0b0d0dedd1b93f1af658df15dd9 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground_2/lib/star.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/lib/star.ma
@@ -154,7 +154,7 @@ lemma NF_to_SN_sn: ∀A,R,S,a. NF_sn A R S a → SN_sn A R S a.
 elim HSa12 -HSa12 /2 width=1/
 qed.
 
-lemma TC_lsub_trans: ∀A,B,R,S. lsub_trans A B R S → lsub_trans A B (LTC … R) S.
+lemma LTC_lsub_trans: ∀A,B,R,S. lsub_trans A B R S → lsub_trans A B (LTC … R) S.
 #A #B #R #S #HRS #L2 #T1 #T2 #H elim H -T2 [ /3 width=3/ ]
 #T #T2 #_ #HT2 #IHT1 #L1 #HL12
 lapply (HRS … HT2 … HL12) -HRS -HT2 /3 width=3/