X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground_2%2Frelocation%2Fnstream_istot.ma;h=0001b90b9c06cff094db74fc2b49b3d54da71815;hb=b9526dac808d40bf89dc378cf9c5ea0c121526a4;hp=c64c7011cd8caab1354a303d976ad67ff98c5e51;hpb=91ab6965be539b7ed0f3208e1c1fffd17aa151f7;p=helm.git

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 c64c7011c..0001b90b9 100644
--- a/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_istot.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_istot.ma
@@ -98,7 +98,8 @@ 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-.
+*)