X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fcomputation%2Fcsn_alt.ma;h=954cb9c014ef7bd600e9bf444b072c3f39f436fb;hb=65008df95049eb835941ffea1aa682c9253c4c2b;hp=d300affdf8ef56865444147f46739d2f2d676b79;hpb=c07e9b0a3e65c28ca4154fec76a54a9a118fa7e1;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/csn_alt.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/csn_alt.ma
index d300affdf..954cb9c01 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/csn_alt.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/csn_alt.ma
@@ -12,6 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
+include "basic_2/notation/relations/snalt_4.ma".
 include "basic_2/computation/cpxs.ma".
 include "basic_2/computation/csn.ma".
 
@@ -66,7 +67,7 @@ lemma csna_intro_cpx: ∀h,g,L,T1. (
 #h #g #L #T1 #H
 @csna_intro_aux #T #T2 #H @(cpxs_ind_dx … H) -T
 [ -H #H destruct #H
-  elim (H ?) //
+  elim H //
 | #T0 #T #HLT1 #HLT2 #IHT #HT10 #HT12 destruct
   elim (term_eq_dec T0 T) #HT0
   [ -HLT1 -HLT2 -H /3 width=1/