update in ground_2 and basic_2

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / rt_computation / cpms_drops.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms_drops.ma
index 0e1d6209049fce3e06a60c49434cd729fbbcce7e..e05d49b0bd0d15eeb0a08540abbdaa3c9c1ffeef 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms_drops.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms_drops.ma
@@ -103,6 +103,19 @@ lemma cpms_delta_drops (n) (h) (G):
 ]
 qed.
 
+lemma cpms_ell_drops (n) (h) (G):
+                     ∀L,K,W,i. ⬇*[i] L ≘ K.ⓛW →
+                     ∀W2. ⦃G, K⦄ ⊢ W ➡*[n, h] W2 →
+                     ∀V2. ⬆*[↑i] W2 ≘ V2 → ⦃G, L⦄ ⊢ #i ➡*[↑n, h] V2.
+#n #h #G #L #K #W #i #HLK #W2 #H @(cpms_ind_dx … H) -W2
+[ /3 width=6 by cpm_cpms, cpm_ell_drops/
+| #n1 #n2 #W1 #W2 #_ #IH #HW12 #V2 #HWV2
+  lapply (drops_isuni_fwd_drop2 … HLK) -HLK // #HLK
+  elim (lifts_total W1 (𝐔❴↑i❵)) #V1 #HWV1 >plus_S1
+  /3 width=11 by cpm_lifts_bi, cpms_step_dx/
+]
+qed.
+
 (* Advanced inversion lemmas ************************************************)
 
 lemma cpms_inv_lref1_drops (n) (h) (G):