partial commit in the relocation component to move some files ...

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

diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_lifts.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_lifts.ma
index 2372488aa5e3170ff880c178f657a0ba9bf77185..109e5e9735fef57e1b477b6b0dff95055a0085eb 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_lifts.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_lifts.ma
@@ -76,12 +76,12 @@ qed-.
 
 (* Basic_2A1: includes: lift_inj *)
 lemma lifts_inj: ∀T1,U,f. ⬆*[f] T1 ≡ U → ∀T2. ⬆*[f] T2 ≡ U → T1 = T2.
-#T1 #U #f #H1 #T2 #H2 lapply (isid_after_dx 𝐈𝐝  f ?)
+#T1 #U #f #H1 #T2 #H2 lapply (isid_after_dx 𝐈𝐝  … f)
 /3 width=6 by lifts_div, lifts_fwd_isid/
 qed-.
 
 (* Basic_2A1: includes: lift_mono *)
 lemma lifts_mono: ∀T,U1,f. ⬆*[f] T ≡ U1 → ∀U2. ⬆*[f] T ≡ U2 → U1 = U2.
-#T #U1 #f #H1 #U2 #H2 lapply (isid_after_sn 𝐈𝐝 f ?)
+#T #U1 #f #H1 #U2 #H2 lapply (isid_after_sn 𝐈𝐝  … f)
 /3 width=6 by lifts_conf, lifts_fwd_isid/
 qed-.