X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground_2%2Frelocation%2Frtmap_sor.ma;h=2a616742ccafe9f67b238217a9b38bab5aa5cf81;hb=9c20dc97d029acbc383aed6b4f0636175a3de609;hp=f86e7f8092784bb8e8ddd8e07c07dc9134aba43e;hpb=045c74915022181e288d9a950cc485437b08d002;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_sor.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_sor.ma
index f86e7f809..2a616742c 100644
--- a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_sor.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_sor.ma
@@ -432,10 +432,18 @@ corec lemma sor_inv_sle_dx: ∀f1,f2,f. f1 ⋓ f2 ≡ f → f2 ⊆ f.
 /3 width=5 by sle_push, sle_next, sle_weak/
 qed-.
 
+lemma sor_inv_sle_sn_trans: ∀f1,f2,f. f1 ⋓ f2 ≡ f → ∀g. g ⊆ f1 → g ⊆ f.
+/3 width=4 by sor_inv_sle_sn, sle_trans/ qed-.
+
+lemma sor_inv_sle_dx_trans: ∀f1,f2,f. f1 ⋓ f2 ≡ f → ∀g. g ⊆ f2 → g ⊆ f.
+/3 width=4 by sor_inv_sle_dx, sle_trans/ qed-.
+
 (* Properties with inclusion ************************************************)
 
-lemma sor_sle_sn: ∀f1,f2,f. f1 ⋓ f2 ≡ f → ∀g. g ⊆ f1 → g ⊆ f.
-/3 width=4 by sor_inv_sle_sn, sle_trans/ qed.
+corec lemma sor_sle_dx: ∀f1,f2. f1 ⊆ f2 → f1 ⋓ f2 ≡ f2.
+#f1 #f2 * -f1 -f2 /3 width=7 by sor_pp, sor_nn, sor_pn/
+qed.
 
-lemma sor_sle_dx: ∀f1,f2,f. f1 ⋓ f2 ≡ f → ∀g. g ⊆ f2 → g ⊆ f.
-/3 width=4 by sor_inv_sle_dx, sle_trans/ qed.
+corec lemma sor_sle_sn: ∀f1,f2. f1 ⊆ f2 → f2 ⋓ f1 ≡ f2.
+#f1 #f2 * -f1 -f2 /3 width=7 by sor_pp, sor_nn, sor_np/
+qed.