updating the dropable-related definitions with coafter ...

[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 0001b90b9c06cff094db74fc2b49b3d54da71815..0bf3c4da85ea1e208e366908b8e5fa9c8224ab68 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
@@ -98,8 +98,6 @@ lemma apply_S1: ∀f,i. (⫯f)@❴i❵ = ⫯(f@❴i❵).
 qed.
 
 (* Main inversion lemmas ****************************************************)
-(*
-lemma apply_inj_aux: ∀f1,f2,j1,j2,i1,i2. f1@❴i1❵ = j1 → f2@❴i2❵ = j2 →
-                     j1 = j2 → f1 ≗ f2 → i1 = i2.
-/2 width=6 by at_inj/ qed-.
-*)
+
+theorem apply_inj: ∀f,i1,i2,j. f@❴i1❵ = j → f@❴i2❵ = j → i1 = i2.
+/2 width=4 by at_inj/ qed-.