\lambda\delta web site update for git

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

diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_istot.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_istot.ma
index d2bd0837e41959f45c6ffea20ddac132992d7611..39211d7f2c74ece3b91c7f155788ca883719e581 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_istot.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_istot.ma
@@ -18,7 +18,7 @@ include "ground_2/relocation/rtmap_istot.ma".
 
 (* RELOCATION N-STREAM ******************************************************)
 
-let rec apply (i: nat) on i: rtmap → nat ≝ ?.
+rec definition apply (i: nat) on i: rtmap → nat ≝ ?.
 * #n #f cases i -i
 [ @n
 | #i lapply (apply i f) -apply -i -f
@@ -48,7 +48,8 @@ lemma at_istot: ∀f. 𝐓⦃f⦄.
 /2 width=2 by ex_intro/ qed.
 
 lemma at_plus2: ∀f,i1,i,n,m. @⦃i1, n@f⦄ ≡ i → @⦃i1, (m+n)@f⦄ ≡ m+i.
-#f #i1 #i #n #m #H elim m -m /2 width=5 by at_next/
+#f #i1 #i #n #m #H elim m -m //
+#m <plus_S1 /2 width=5 by at_next/ (**) (* full auto fails *)
 qed.
 
 (* Specific inversion lemmas on at ******************************************)