partial commit in static_2

[helm.git] / matita / matita / contribs / lambdadelta / static_2 / relocation / sex_tc.ma

diff --git a/matita/matita/contribs/lambdadelta/static_2/relocation/sex_tc.ma b/matita/matita/contribs/lambdadelta/static_2/relocation/sex_tc.ma
index 379cfc75146fdc8ff995e03bd8024a131e71cad9..0a95ed3b0f5720832af36230e9b3f61c57061157 100644 (file)
--- a/matita/matita/contribs/lambdadelta/static_2/relocation/sex_tc.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/relocation/sex_tc.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "ground_2/lib/star.ma".
+include "ground/lib/star.ma".
 include "static_2/relocation/sex.ma".
 
 (* GENERIC ENTRYWISE EXTENSION OF CONTEXT-SENSITIVE REALTIONS FOR TERMS *****)
@@ -87,8 +87,8 @@ theorem sex_tc_step_dx: ∀RN,RP. s_rs_transitive_isid RN RP →
 #RN #RP #HRP #f #L1 #L #H elim H -f -L1 -L
 [ #f #_ #Y #H -HRP >(sex_inv_atom1 … H) -Y // ]
 #f #I1 #I #L1 #L #HL1 #HI1 #IH #Hf #Y #H
-[ elim (isid_inv_next … Hf) -Hf //
-| lapply (isid_inv_push … Hf ??) -Hf [3: |*: // ] #Hf
+[ elim (pr_isi_inv_next … Hf) -Hf //
+| lapply (pr_isi_inv_push … Hf ??) -Hf [3: |*: // ] #Hf
   elim (sex_inv_push1 … H) -H #I2 #L2 #HL2 #HI2 #H destruct
   @sex_push [ /2 width=1 by/ ] -L2 -IH
   @(TC_strap … HI1) -HI1