X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frt_computation%2Fcprs_drops.ma;h=bd1afeec3492043b8bf47e684b8862d7013e525e;hp=19829738f5f4f473c8f21c90f4a670b3c1b1dead;hb=f308429a0fde273605a2330efc63268b4ac36c99;hpb=87f57ddc367303c33e19c83cd8989cd561f3185b

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cprs_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cprs_drops.ma
index 19829738f..bd1afeec3 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cprs_drops.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cprs_drops.ma
@@ -20,9 +20,9 @@ include "basic_2/rt_computation/cpms_drops.ma".
 
 (* Basic_1: was: pr3_gen_lref *)
 (* Basic_2A1: was: cprs_inv_lref1 *)
-lemma cprs_inv_lref1_drops (h) (G): ∀L,T2,i. ⦃G, L⦄ ⊢ #i ➡*[h] T2 →
+lemma cprs_inv_lref1_drops (h) (G): ∀L,T2,i. ⦃G,L⦄ ⊢ #i ➡*[h] T2 →
                                     ∨∨ T2 = #i
-                                     | ∃∃K,V1,T1. ⬇*[i] L ≘ K.ⓓV1 & ⦃G, K⦄ ⊢ V1 ➡*[h] T1 &
+                                     | ∃∃K,V1,T1. ⬇*[i] L ≘ K.ⓓV1 & ⦃G,K⦄ ⊢ V1 ➡*[h] T1 &
                                                   ⬆*[↑i] T1 ≘ T2.
 #h #G #L #T2 #i #H elim (cpms_inv_lref1_drops … H) -H *
 [ /2 width=1 by or_introl/