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=ea83c19f4cac864dd87eb059d8aeb2343eba480f;hp=a4117b5963e3e1e8ec4053d0ed8ac46270bb8dec;hpb=a8c166f1e1baeeae04553058bd179420ada8bbe7;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 a4117b596..78a9b4987 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/grammar/tstc.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/grammar/tstc.ma
@@ -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-.