update in static_2

[helm.git] / matita / matita / contribs / lambdadelta / static_2 / relocation / seq_seq.ma

diff --git a/matita/matita/contribs/lambdadelta/static_2/relocation/seq_seq.ma b/matita/matita/contribs/lambdadelta/static_2/relocation/seq_seq.ma
index a06f1f52758d6fe077bc4442bda2aa01a068762d..98bc91580c289e1c87e919ef0b07e8408bdd67cd 100644 (file)
--- a/matita/matita/contribs/lambdadelta/static_2/relocation/seq_seq.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/relocation/seq_seq.ma
@@ -12,26 +12,31 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "static_2/syntax/ceq_ext_ceq_ext.ma".
+include "static_2/syntax/teq_ext_teq_ext.ma".
 include "static_2/relocation/sex_sex.ma".
 
 (* SYNTACTIC EQUIVALENCE FOR SELECTED LOCAL ENVIRONMENTS ********************)
 
 (* Main properties **********************************************************)
 
-theorem seq_trans: ∀f. Transitive … (seq f).
+theorem seq_trans (f):
+        Transitive … (seq f).
 /3 width=5 by sex_trans, ceq_ext_trans/ qed-.
 
-theorem seq_canc_sn: ∀f. left_cancellable … (seq f).
+theorem seq_canc_sn (f):
+        left_cancellable … (seq f).
 /3 width=3 by sex_canc_sn, seq_trans, seq_sym/ qed-.
 
-theorem seq_canc_dx: ∀f. right_cancellable … (seq f).
+theorem seq_canc_dx (f):
+        right_cancellable … (seq f).
 /3 width=3 by sex_canc_dx, seq_trans, seq_sym/ qed-.
 
-theorem seq_join: ∀f1,L1,L2. L1 ≡[f1] L2 → ∀f2. L1 ≡[f2] L2 →
-                  ∀f. f1 ⋓ f2 ≘ f → L1 ≡[f] L2.
+theorem seq_join:
+        ∀f1,L1,L2. L1 ≡[f1] L2 → ∀f2. L1 ≡[f2] L2 →
+        ∀f. f1 ⋓ f2 ≘ f → L1 ≡[f] L2.
 /2 width=5 by sex_join/ qed-.
 
-theorem seq_meet: ∀f1,L1,L2. L1 ≡[f1] L2 → ∀f2. L1 ≡[f2] L2 →
-                  ∀f. f1 ⋒ f2 ≘ f → L1 ≡[f] L2.
+theorem seq_meet:
+        ∀f1,L1,L2. L1 ≡[f1] L2 → ∀f2. L1 ≡[f2] L2 →
+        ∀f. f1 ⋒ f2 ≘ f → L1 ≡[f] L2.
 /2 width=5 by sex_meet/ qed-.