]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_cpcs.ma
update in basic_2 and apps_2
[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / dynamic / nta_cpcs.ma
index 4d695a3ec8db85bc17d5d86542a66d466d3e90e6..0dd3441f203dfa970266856826744527d7b7daaa 100644 (file)
@@ -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-.