X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fcomputation%2Fcprs_cprs.ma;h=3f2754bd569b4ffda646d21d9db433252c4789c9;hb=52e675f555f559c047d5449db7fc89a51b977d35;hp=8b073c157152018b84a52850fa8c1dfcb6678a55;hpb=75fac6d60f67a4dfa38ea6c2cc45a18eda5d8996;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cprs_cprs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cprs_cprs.ma
index 8b073c157..3f2754bd5 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/cprs_cprs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/cprs_cprs.ma
@@ -108,7 +108,7 @@ lemma lpr_cpr_trans: ∀G. s_r_transitive … (cpr G) (λ_. lpr G).
 #G #L2 #T1 #T2 #HT12 elim HT12 -G -L2 -T1 -T2
 [ /2 width=3 by/
 | #G #L2 #K2 #V0 #V2 #W2 #i #HLK2 #_ #HVW2 #IHV02 #L1 #HL12
-  elim (lpr_ldrop_trans_O1 … HL12 … HLK2) -L2 #X #HLK1 #H
+  elim (lpr_drop_trans_O1 … HL12 … HLK2) -L2 #X #HLK1 #H
   elim (lpr_inv_pair2 … H) -H #K1 #V1 #HK12 #HV10 #H destruct
   /4 width=6 by cprs_strap2, cprs_delta/
 |3,7: /4 width=1 by lpr_pair, cprs_bind, cprs_beta/