X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frt_computation%2Fcpms_drops.ma;h=e05d49b0bd0d15eeb0a08540abbdaa3c9c1ffeef;hp=0e1d6209049fce3e06a60c49434cd729fbbcce7e;hb=ede00573e3e4cb28df7ca9a5dae6228c2b432608;hpb=1083ac3b1acac5f1ac1fa40a9a417dd9d268dced

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 0e1d62090..e05d49b0b 100644
--- 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):