X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambda_delta%2FBasic_2%2Funfold%2Flifts.ma;h=6a3c647a0cfa2b10674332c5fdd78f84fb52c192;hb=44c1079dabf1d3c0b69d0155ddbaea8627ec901c;hp=40f4325b1c45450b71ab088bfdf9486e723510c7;hpb=48b202cd4ccd3ffc10f9a134314f747fdee30d36;p=helm.git

diff --git a/matita/matita/contribs/lambda_delta/Basic_2/unfold/lifts.ma b/matita/matita/contribs/lambda_delta/Basic_2/unfold/lifts.ma
index 40f4325b1..6a3c647a0 100644
--- a/matita/matita/contribs/lambda_delta/Basic_2/unfold/lifts.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/unfold/lifts.ma
@@ -13,7 +13,7 @@
 (**************************************************************************)
 
 include "Basic_2/substitution/lift.ma".
-include "Basic_2/unfold/gr2.ma".
+include "Basic_2/unfold/gr2_plus.ma".
 
 (* GENERIC TERM RELOCATION **************************************************)
 
@@ -112,11 +112,11 @@ qed-.
 
 (* Basic forward lemmas *****************************************************)
 
-lemma lifts_simple_dx: ∀T1,T2,des. ⇧*[des] T1 ≡ T2 → 𝕊[T1] → 𝕊[T2].
+lemma lifts_simple_dx: ∀T1,T2,des. ⇧*[des] T1 ≡ T2 → 𝐒[T1] → 𝐒[T2].
 #T1 #T2 #des #H elim H -T1 -T2 -des // /3 width=5 by lift_simple_dx/
 qed-.
 
-lemma lifts_simple_sn: ∀T1,T2,des. ⇧*[des] T1 ≡ T2 → 𝕊[T2] → 𝕊[T1].
+lemma lifts_simple_sn: ∀T1,T2,des. ⇧*[des] T1 ≡ T2 → 𝐒[T2] → 𝐒[T1].
 #T1 #T2 #des #H elim H -T1 -T2 -des // /3 width=5 by lift_simple_sn/
 qed-.