lambdadelta

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / computation / csn_alt.ma

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 d300affdf8ef56865444147f46739d2f2d676b79..954cb9c014ef7bd600e9bf444b072c3f39f436fb 100644 (file)
--- 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/