X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambda_delta%2Fbasic_2%2Fcomputation%2Fcprs_lift.ma;fp=matita%2Fmatita%2Fcontribs%2Flambda_delta%2Fbasic_2%2Fcomputation%2Fcprs_lift.ma;h=11ce81ff8e1706e18f9a8cedd97c0ad78041e641;hb=b8a7401daf0637a4ce8f86e960b180cb5f22ecb3;hp=32dcb2ce95b9151a4ece3438bcaa5de631261e9f;hpb=efb9979fe0496c30ea9b8ce6ed9f89e41413ea2d;p=helm.git

diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_lift.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_lift.ma
index 32dcb2ce9..11ce81ff8 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_lift.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_lift.ma
@@ -70,4 +70,3 @@ lemma cprs_inv_lift: ∀L,K,d,e. ⇩[d, e] L ≡ K →
 -HTU1 #U #U2 #_ #HU2 * #T #HTU #HT1
 elim (cpr_inv_lift … HLK … HTU … HU2) -U -HLK /3 width=5/
 qed.
-