X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fetc%2Fcpys2%2Flsuby.etc;fp=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fetc%2Fcpys2%2Flsuby.etc;h=657ad6b6eb58330fb3938264c2db4b564b22bdd6;hb=c671743a83bbc7fff114e3e3694f628c0ec6685b;hp=0000000000000000000000000000000000000000;hpb=a8e31c02eefecdcd7d8a893c9f0a036a30fa57e4;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/cpys2/lsuby.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cpys2/lsuby.etc
new file mode 100644
index 000000000..657ad6b6e
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/etc/cpys2/lsuby.etc
@@ -0,0 +1,15 @@
+(*
+lemma lsuby_weak: ∀L1,L2,d1,e1. L1 ⊑×[d1, e1] L2 →
+                  ∀d2,e2. d1 ≤ d2 → e2 ≤ e1 → L1 ⊑×[d2, e2] L2.
+#L1 #L2 #d1 #e1 #H elim H -L1 -L2 -d1 -e1 //
+[ #I1 #I2 #L1 #L2 #V1 #V2 #HL12 #_ #d2 #e2 #_ #He21
+  >(yle_inv_O2 … He21) -He21
+  /4 width=3 by lsuby_fwd_length, lsuby_O1, monotonic_le_plus_l/
+| #I1 #I2 #L1 #L2 #V #e #HL12 #IHL12 #d2 #e2 #_ #He21
+  elim (ynat_cases e2) /4 width=3 by lsuby_fwd_length, lsuby_O1, monotonic_le_plus_l/
+  * #e0 #H destruct lapply (yle_inv_succ … He21) -He21 #He21
+  elim (ynat_cases d2) /3 width=1 by lsuby_pair/
+  * #d0 #H destruct @lsuby_succ @IHL12 //
+  [   destruct
+  
+*)