update in ground_2 and basic_2

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / relocation / lexs_tc.ma

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 24d8d9fcf2934287140ed980f63e086117adfbae..70cfdbd7156e52ac88b9a31459a4e84b9d1e71ed 100644 (file)
--- 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