X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frelocation%2Flex.ma;h=5c76651b2e4f117327b24fa460f567f2f268c091;hb=397413c4196f84c81d61ba7dd79b54ab1c428ebb;hp=7e4e03c8ece5efba6c33b9af30c2d044d1e20a56;hpb=24ba1bb3f67505d3e384747ff90d26d3996bd3f5;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lex.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lex.ma
index 7e4e03c8e..5c76651b2 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/relocation/lex.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lex.ma
@@ -54,7 +54,7 @@ qed-.
 lemma lex_inv_bind_sn: ∀R,I1,L2,K1. K1.ⓘ{I1} ⪤[R] L2 →
                        ∃∃I2,K2. K1 ⪤[R] K2 & cext2 R K1 I1 I2 & L2 = K2.ⓘ{I2}.
 #R #I1 #L2 #K1 * #f #Hf #H
-lapply (lexs_eq_repl_fwd … H (↑f) ?) -H /2 width=1 by eq_push_inv_isid/ #H
+lapply (lexs_eq_repl_fwd … H (⫯f) ?) -H /2 width=1 by eq_push_inv_isid/ #H
 elim (lexs_inv_push1 … H) -H #I2 #K2 #HK12 #HI12 #H destruct
 /3 width=5 by ex2_intro, ex3_2_intro/
 qed-.
@@ -67,7 +67,7 @@ qed-.
 lemma lex_inv_bind_dx: ∀R,I2,L1,K2. L1 ⪤[R] K2.ⓘ{I2} →
                        ∃∃I1,K1. K1 ⪤[R] K2 & cext2 R K1 I1 I2 & L1 = K1.ⓘ{I1}.
 #R #I2 #L1 #K2 * #f #Hf #H
-lapply (lexs_eq_repl_fwd … H (↑f) ?) -H /2 width=1 by eq_push_inv_isid/ #H
+lapply (lexs_eq_repl_fwd … H (⫯f) ?) -H /2 width=1 by eq_push_inv_isid/ #H
 elim (lexs_inv_push2 … H) -H #I1 #K1 #HK12 #HI12 #H destruct
 /3 width=5 by ex3_2_intro, ex2_intro/
 qed-.