X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fapps_2%2Fetc%2Fmodels%2Fvdrop_old.etc;h=d7dd140ac4df6ac5b3c61af186b9fc156ba7bfc7;hp=5a857fbb18100add93281751c1f8603c2b069f1a;hb=cc600ed1e115d5566947288d532a1e89d989227f;hpb=ea918ec7701db4458c5ca25885e80abc6fed1be7

diff --git a/matita/matita/contribs/lambdadelta/apps_2/etc/models/vdrop_old.etc b/matita/matita/contribs/lambdadelta/apps_2/etc/models/vdrop_old.etc
index 5a857fbb1..d7dd140ac 100644
--- a/matita/matita/contribs/lambdadelta/apps_2/etc/models/vdrop_old.etc
+++ b/matita/matita/contribs/lambdadelta/apps_2/etc/models/vdrop_old.etc
@@ -1,4 +1,9 @@
-
+lemma pippo: ∀M,v1,v2,d,i. [i⬐d] v1 ≐⦋M⦌ v2 → v1 ≐⦋M⦌ ↓[i,1] v2.
+#M #v1 #v2 #d #i #H #j elim (lt_or_ge … j i) #Hij
+[ >lower_lt // <(H j) >raise_lt //
+| >lower_ge // <(H (j+1)) >raise_gt /2 width=1 by le_S_S/
+]
+qed-.
 
 lemma vdrop_refl: ∀M,v,l. ↓[l, 0] v ≐⦋M⦌ v.
 #M #v #l #i elim (lt_or_ge … i l) #Hil