From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Sat, 7 Sep 2013 17:11:03 +0000 (+0000)
Subject: previous commit continued :)
X-Git-Tag: make_still_working~1108
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=efff5b0361797c9eb4c5ac8acc75488d3cf2ccb7;p=helm.git

previous commit continued :)
---

diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop.ma
index 6acb2858c..94c6b0f73 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop.ma
@@ -12,6 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
+include "ground_2/lstar.ma".
 include "basic_2/notation/relations/rdrop_4.ma".
 include "basic_2/grammar/lenv_length.ma".
 include "basic_2/grammar/lenv_weight.ma".
@@ -234,6 +235,16 @@ lemma dropable_dx_TC: ∀R. dropable_dx R → dropable_dx (TC … R).
 ]
 qed.
 
+lemma l_deliftable_sn_llstar: ∀R. l_deliftable_sn R →
+                              ∀l. l_deliftable_sn (llstar … R l).
+#R #HR #l #L #U1 #U2 #H @(lstar_ind_r … l U2 H) -l -U2
+[ /2 width=3/
+| #l #U #U2 #_ #HU2 #IHU1 #K #d #e #HLK #T1 #HTU1
+  elim (IHU1 … HLK … HTU1) -IHU1 -U1 #T #HTU #HT1
+  elim (HR … HU2 … HLK … HTU) -HR -L -U /3 width=5/
+]
+qed.
+
 (* Basic forvard lemmas *****************************************************)
 
 (* Basic_1: was: drop_S *)
diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop_ldrop.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop_ldrop.ma
index 386884296..00691d9f3 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop_ldrop.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop_ldrop.ma
@@ -137,6 +137,15 @@ axiom ldrop_div: ∀e1,L1,L. ⇩[0, e1] L1 ≡ L → ∀e2,L2. ⇩[0, e2] L2 ≡
 
 (* Advanced properties ******************************************************)
 
+lemma l_liftable_llstar: ∀R. l_liftable R → ∀l. l_liftable (llstar … R l).
+#R #HR #l #K #T1 #T2 #H @(lstar_ind_r … l T2 H) -l -T2
+[ #L #d #e #_ #U1 #HTU1 #U2 #HTU2 -HR -K
+  >(lift_mono … HTU2 … HTU1) -T1 -U2 -d -e //
+| #l #T #T2 #_ #HT2 #IHT1 #L #d #e #HLK #U1 #HTU1 #U2 #HTU2
+  elim (lift_total T d e) /3 width=11 by lstar_dx/ (**) (* auto too slow without trace *)
+]
+qed.
+
 (* Basic_1: was: drop_conf_lt *)
 lemma ldrop_conf_lt: ∀d1,e1,L,L1. ⇩[d1, e1] L ≡ L1 →
                      ∀e2,K2,I,V2. ⇩[0, e2] L ≡ K2. ⓑ{I} V2 →