X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fstatic_2%2Frelocation%2Fseq_seq.ma;h=98bc91580c289e1c87e919ef0b07e8408bdd67cd;hp=a06f1f52758d6fe077bc4442bda2aa01a068762d;hb=b118146b97959e6a6dde18fdd014b8e1e676a2d1;hpb=613d8642b1154dde0c026cbdcd96568910198251

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 a06f1f527..98bc91580 100644
--- 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-.