advances towards confluence of reduction in local environments ...

[helm.git] / matita / matita / contribs / lambdadelta / ground_2 / relocation / rtmap_sor.ma

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 2a616742ccafe9f67b238217a9b38bab5aa5cf81..efa6b54d9d60f1078d6b26672fa5d1c9615ce17a 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_sor.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_sor.ma
@@ -438,6 +438,8 @@ lemma sor_inv_sle_sn_trans: ∀f1,f2,f. f1 ⋓ f2 ≡ f → ∀g. g ⊆ f1 → g
 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-.
 
+axiom sor_inv_sle: ∀f1,f2,f. f1 ⋓ f2 ≡ f → ∀g. f1 ⊆ g → f2 ⊆ g → f ⊆ g.
+
 (* Properties with inclusion ************************************************)
 
 corec lemma sor_sle_dx: ∀f1,f2. f1 ⊆ f2 → f1 ⋓ f2 ≡ f2.