X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambda%2Fpaths%2Fstandard_precedence.ma;h=a4ff9e9fbdb7f3e297a551e6af456f5c1985c30f;hb=5c35602808c464a9098b3f39afb7dced059e0d6d;hp=e67a96d0402808750961c5c15175eb10210824c6;hpb=dabd7add16b4e678f48bc15cd0d992b80fbc9216;p=helm.git

diff --git a/matita/matita/contribs/lambda/paths/standard_precedence.ma b/matita/matita/contribs/lambda/paths/standard_precedence.ma
index e67a96d04..a4ff9e9fb 100644
--- a/matita/matita/contribs/lambda/paths/standard_precedence.ma
+++ b/matita/matita/contribs/lambda/paths/standard_precedence.ma
@@ -40,6 +40,17 @@ lemma sprec_inv_sn: ∀p,q. p ≺ q → ∀p0. sn::p0 = p →
 ]
 qed-.
 
+lemma sprec_inv_dx: ∀p,q. p ≺ q → ∀q0. dx::q0 = q →
+                    ◊ = p ∨ ∃∃p0. p0 ≺ q0 & dx::p0 = p.
+#p #q * -p -q
+[ #o #q #q0 #H destruct /2 width=1/
+| #p #q #q0 #H destruct
+| #p #q #q0 #H destruct
+| #o #p #q #Hpq #q0 #H destruct /3 width=3/
+| #q0 #H destruct
+]
+qed-.
+
 lemma sprec_inv_rc: ∀p,q. p ≺ q → ∀p0. rc::p0 = p →
                     (∃∃q0. p0 ≺ q0 & rc::q0 = q) ∨
                     ∃q0. sn::q0 = q.
@@ -70,3 +81,7 @@ lemma sprec_fwd_in_whd: ∀p,q. p ≺ q → in_whd q → in_whd p.
 | #o #p #q #_ #IHpq * #H destruct /3 width=1/
 ]
 qed-.
+
+lemma sprec_fwd_in_inner: ∀p,q. p ≺ q → in_inner p → in_inner q.
+/3 width=3 by sprec_fwd_in_whd/
+qed-.