X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fgrammar%2Ftstc.ma;h=defc91ed95e244b5040bc87b939e6d1104373986;hb=02df4ecb9d5ad173a3e306952cc09d83b62cfdcf;hp=78a9b4987a4d5a938cbfba3ebe7de73416ad81f6;hpb=e8998d29ab83e7b6aa495a079193705b2f6743d3;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/grammar/tstc.ma b/matita/matita/contribs/lambdadelta/basic_2/grammar/tstc.ma
index 78a9b4987..defc91ed9 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/grammar/tstc.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/grammar/tstc.ma
@@ -12,6 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
+include "basic_2/notation/relations/iso_2.ma".
 include "basic_2/grammar/term_simple.ma".
 
 (* SAME TOP TERM CONSTRUCTOR ************************************************)
@@ -80,7 +81,7 @@ qed.
 
 lemma tstc_dec: ∀T1,T2. Decidable (T1 ≃ T2).
 * #I1 [2: #V1 #T1 ] * #I2 [2,4: #V2 #T2 ]
-[ elim (item2_eq_dec I1 I2) #HI12
+[ elim (eq_item2_dec I1 I2) #HI12
   [ destruct /2 width=1/
   | @or_intror #H
     elim (tstc_inv_pair1 … H) -H #V #T #H destruct /2 width=1/
@@ -89,7 +90,7 @@ lemma tstc_dec: ∀T1,T2. Decidable (T1 ≃ T2).
   lapply (tstc_inv_atom1 … H) -H #H destruct
 | @or_intror #H
   lapply (tstc_inv_atom2 … H) -H #H destruct
-| elim (item0_eq_dec I1 I2) #HI12
+| elim (eq_item0_dec I1 I2) #HI12
   [ destruct /2 width=1/
   | @or_intror #H
     lapply (tstc_inv_atom2 … H) -H #H destruct /2 width=1/