- bug fix in the induction for the closure property

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / grammar / tstc.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/grammar/tstc.ma b/matita/matita/contribs/lambdadelta/basic_2/grammar/tstc.ma
index 78a9b4987a4d5a938cbfba3ebe7de73416ad81f6..defc91ed95e244b5040bc87b939e6d1104373986 100644 (file)
--- 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/