lambda_delta: partial commit ...

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

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 c4c44c9f323baad7933a424691d0b558ff3a3379..78a9b4987a4d5a938cbfba3ebe7de73416ad81f6 100644 (file)
--- 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-.