X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frelocation%2Flexs_tc.ma;h=70cfdbd7156e52ac88b9a31459a4e84b9d1e71ed;hp=24d8d9fcf2934287140ed980f63e086117adfbae;hb=990f97071a9939d47be16b36f6045d3b23f218e0;hpb=42705ef31dd3513a998533e02b5f20fb38dd4fb2

diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs_tc.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs_tc.ma
index 24d8d9fcf..70cfdbd71 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs_tc.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs_tc.ma
@@ -98,7 +98,6 @@ qed-.
 
 (* Advanced properties ******************************************************)
 
-(* Basic_2A1: uses: TC_lpx_sn_inv_lpx_sn_LTC *)
 lemma lexs_tc_dx: ∀RN,RP. s_rs_transitive_isid RN RP →
                   ∀f. 𝐈⦃f⦄ → ∀L1,L2. TC … (lexs RN RP f) L1 L2 → L1 ⪤*[RN, LTC … RP, f] L2.
 #RN #RP #HRP #f #Hf #L1 #L2 #H @(TC_ind_dx ??????? H) -L1
@@ -113,7 +112,6 @@ lemma lexs_inv_tc_sn: ∀RN,RP. c_reflexive … RN → c_reflexive … RP →
 /2 width=1 by lexs_tc_next, lexs_tc_push_sn, lexs_atom, inj/
 qed-.
 
-(* Basic_2A1: uses: lpx_sn_LTC_TC_lpx_sn *)
 lemma lexs_inv_tc_dx: ∀RN,RP. c_reflexive … RN → c_reflexive … RP →
                       ∀f,L1,L2. L1 ⪤*[RN, LTC … RP, f] L2 → TC … (lexs RN RP f) L1 L2.
 #RN #RP #HRN #HRP #f #L1 #L2 #H elim H -f -L1 -L2