X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fdynamic%2Fnta_cpcs.ma;h=0dd3441f203dfa970266856826744527d7b7daaa;hp=4d695a3ec8db85bc17d5d86542a66d466d3e90e6;hb=0c302a9fda708e5019e48d14c5419a8a65190745;hpb=5c92c318030a05c766b3f6070dbd23589cbdee04

diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_cpcs.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_cpcs.ma
index 4d695a3ec..0dd3441f2 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_cpcs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_cpcs.ma
@@ -50,4 +50,3 @@ elim (cnv_inv_cast … H) -H #X1 #HX2 #_ #HX21 #H
 lapply (cpms_inv_sort1 … H) -H #H destruct
 /2 width=1 by cpcs_cprs_sn/
 qed-.
-