milestone in basic_2 with additions in static_2

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / dynamic / nta_cpms.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_cpms.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_cpms.ma
index 8dbb60c79088b3d04297b6d317cfc577d2044d70..b0530a3bbc83553df50ebc994252c6c58a48bb68 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_cpms.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_cpms.ma
@@ -58,6 +58,6 @@ elim (cnv_inv_cast … H) -H #X #HWU #HWT #HUX #HTX
 elim (cnv_inv_bind … HWU) -HWU #HW #HU
 elim (cnv_inv_bind … HWT) -HWT #_ #HT
 elim (cpms_inv_abst_sn … HUX) -HUX #W0 #X0 #_ #HUX0 #H destruct
-elim (cpms_inv_abst_bi … HTX) -HTX #_ #HTX0 -W0
+elim (cpms_inv_abst_bi … HTX) -HTX #_ #_ #HTX0 -W0
 /3 width=3 by cnv_cast, conj/
 qed-.