- more on subject reduction of atomic arity assignment

[helm.git] / matita / matita / contribs / lambda_delta / basic_2 / computation / cprs_lift.ma

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 32dcb2ce95b9151a4ece3438bcaa5de631261e9f..11ce81ff8e1706e18f9a8cedd97c0ad78041e641 100644 (file)
--- 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.
-