lift functions and identity map

[helm.git] / matita / matita / contribs / lambdadelta / ground_2 / relocation / nstream_after.ma

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 154ba25e3fbb76df3a449d9ff5eedc5e67833952..cf5a6b6ebb038189001d91270ebd75c3f4bd7c39 100644 (file)
--- 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 *******************************************)