X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambda_delta%2FBasic_2%2Fcomputation%2Fcsn.ma;fp=matita%2Fmatita%2Fcontribs%2Flambda_delta%2FBasic_2%2Fcomputation%2Fcsn.ma;h=043fa9a277e25087e892c2805158f7b480052a7d;hb=16bbb2d6b16d5647d944f18f0fd6d4dd3df431fe;hp=f5d8b739017588a8c6ea96faaf7562b9551ac55f;hpb=0ea1af833c4fd9205f047072518e1aabf7987945;p=helm.git

diff --git a/matita/matita/contribs/lambda_delta/Basic_2/computation/csn.ma b/matita/matita/contribs/lambda_delta/Basic_2/computation/csn.ma
index f5d8b7390..043fa9a27 100644
--- a/matita/matita/contribs/lambda_delta/Basic_2/computation/csn.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/computation/csn.ma
@@ -62,7 +62,7 @@ lemma csn_cast: ∀L,W. L ⊢ ⬇* W → ∀T. L ⊢ ⬇* T → L ⊢ ⬇* ⓣW.
 @csn_intro #X #H1 #H2
 elim (cpr_inv_cast1 … H1) -H1
 [ * #W0 #T0 #HLW0 #HLT0 #H destruct
-  elim (eq_false_inv_tpair … H2) -H2
+  elim (eq_false_inv_tpair_sn … H2) -H2
   [ /3 width=3/
   | -HLW0 * #H destruct /3 width=1/ 
   ]