- ldrop is now drop as in basic_1

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

diff --git a/matita/matita/contribs/lambdadelta/basic_2/grammar/tstc_tstc.ma b/matita/matita/contribs/lambdadelta/basic_2/grammar/tstc_tstc.ma
index df6fe3729856461538f682589b18cc4696628971..83a17a67950f7e4b1601415f9eadacc941ba9e9e 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/grammar/tstc_tstc.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/grammar/tstc_tstc.ma
@@ -19,14 +19,14 @@ include "basic_2/grammar/tstc.ma".
 (* Main properties **********************************************************)
 
 (* Basic_1: was: iso_trans *)
-theorem tstc_trans: ∀T1,T. T1 ≃ T → ∀T2. T ≃ T2 → T1 ≃ T2.
+theorem tstc_trans: Transitive … tstc.
 #T1 #T * -T1 -T //
 #I #V1 #V #T1 #T #X #H
 elim (tstc_inv_pair1 … H) -H #V2 #T2 #H destruct //
-qed.
+qed-.
 
-theorem tstc_canc_sn: â\88\80T,T1. T â\89\83 T1 â\86\92 â\88\80T2. T â\89\83 T2 â\86\92 T1 â\89\83 T2.
-/3 width=3/ qed.
+theorem tstc_canc_sn: â\88\80T,T1. T â\89\82 T1 â\86\92 â\88\80T2. T â\89\82 T2 â\86\92 T1 â\89\82 T2.
+/3 width=3 by tstc_trans, tstc_sym/ qed-.
 
-theorem tstc_canc_dx: â\88\80T1,T. T1 â\89\83 T â\86\92 â\88\80T2. T2 â\89\83 T â\86\92 T1 â\89\83 T2.
-/3 width=3/ qed.
+theorem tstc_canc_dx: â\88\80T1,T. T1 â\89\82 T â\86\92 â\88\80T2. T2 â\89\82 T â\86\92 T1 â\89\82 T2.
+/3 width=3 by tstc_trans, tstc_sym/ qed-.