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

diff --git a/matita/matita/contribs/lambda_delta/basic_2/grammar/tstc.ma b/matita/matita/contribs/lambda_delta/basic_2/grammar/tstc.ma
index c4c44c9f3..78a9b4987 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/grammar/tstc.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/grammar/tstc.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "Basic_2/grammar/term_simple.ma".
+include "basic_2/grammar/term_simple.ma".
 
 (* SAME TOP TERM CONSTRUCTOR ************************************************)
 
@@ -97,11 +97,11 @@ lemma tstc_dec: ∀T1,T2. Decidable (T1 ≃ T2).
 ]
 qed.
 
-lemma simple_tstc_repl_dx: ∀T1,T2. T1 ≃ T2 → 𝐒[T1] → 𝐒[T2].
+lemma simple_tstc_repl_dx: ∀T1,T2. T1 ≃ T2 → 𝐒⦃T1⦄ → 𝐒⦃T2⦄.
 #T1 #T2 * -T1 -T2 //
 #I #V1 #V2 #T1 #T2 #H
 elim (simple_inv_pair … H) -H #J #H destruct //
 qed. (**) (* remove from index *)
 
-lemma simple_tstc_repl_sn: ∀T1,T2. T1 ≃ T2 → 𝐒[T2] → 𝐒[T1].
+lemma simple_tstc_repl_sn: ∀T1,T2. T1 ≃ T2 → 𝐒⦃T2⦄ → 𝐒⦃T1⦄.
 /3 width=3/ qed-.