X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground_2%2Frelocation%2Fnstream_after.ma;h=cf5a6b6ebb038189001d91270ebd75c3f4bd7c39;hb=4b8544042a6f3c5f5d303d4120c69abbc34ce15b;hp=154ba25e3fbb76df3a449d9ff5eedc5e67833952;hpb=7d8ebeb7b6f21204b88786c738c67f52f3703c5b;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_after.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_after.ma
index 154ba25e3..cf5a6b6eb 100644
--- a/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_after.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_after.ma
@@ -420,14 +420,15 @@ let corec after_mono: ∀t1,t2,x. t1 ⊚ t2 ≡ x → ∀y. t1 ⊚ t2 ≡ y →
 * #a1 #t1 * #a2 #t2 * #c #x #Hx * #d #y #Hy
 cases (after_inv_apply … Hx) -Hx #Hc #Hx
 cases (after_inv_apply … Hy) -Hy #Hd #Hy
-/3 width=4 by eq_sec/
+/3 width=4 by eq_seq/
 qed-.
 
 let corec after_inj: ∀t1,x,t. t1 ⊚ x ≡ t → ∀y. t1 ⊚ y ≡ t → x ≐ y ≝ ?.
 * #a1 #t1 * #c #x * #a #t #Hx * #d #y #Hy
 cases (after_inv_apply … Hx) -Hx #Hc #Hx
 cases (after_inv_apply … Hy) -Hy #Hd
-cases (apply_inj_aux … Hc Hd) #Hy -a -d /3 width=4 by eq_sec/
+cases (apply_inj_aux … Hc Hd) //
+#Hy -a -d /3 width=4 by eq_seq/
 qed-.
 
 (* Main inversion lemmas on after *******************************************)