X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fmatita%2Fcontribs%2Flambda%2Fpaths%2Fstandard_precedence.ma;fp=matita%2Fmatita%2Fcontribs%2Flambda%2Fpaths%2Fstandard_precedence.ma;h=e67a96d0402808750961c5c15175eb10210824c6;hb=4853e6e91abc124f9e6db1006cd731dbcf5708b9;hp=a55770aa8374f816a745108ea9c0b5a58a70d1c4;hpb=2a11039cffb66439322ef7d3cf5eb6f241c33d16;p=helm.git

diff --git a/matita/matita/contribs/lambda/paths/standard_precedence.ma b/matita/matita/contribs/lambda/paths/standard_precedence.ma
index a55770aa8..e67a96d04 100644
--- a/matita/matita/contribs/lambda/paths/standard_precedence.ma
+++ b/matita/matita/contribs/lambda/paths/standard_precedence.ma
@@ -40,6 +40,29 @@ lemma sprec_inv_sn: ∀p,q. p ≺ q → ∀p0. sn::p0 = p →
 ]
 qed-.
 
+lemma sprec_inv_rc: ∀p,q. p ≺ q → ∀p0. rc::p0 = p →
+                    (∃∃q0. p0 ≺ q0 & rc::q0 = q) ∨
+                    ∃q0. sn::q0 = q.
+#p #q * -p -q
+[ #o #q #p0 #H destruct
+| #p #q #p0 #H destruct
+| #p #q #p0 #H destruct /3 width=2/
+| #o #p #q #Hpq #p0 #H destruct /3 width=3/
+| #p0 #H destruct
+]
+qed-.
+
+lemma sprec_inv_comp: ∀p1,p2. p1 ≺ p2 →
+                      ∀o,q1,q2. o::q1 = p1 → o::q2 = p2 → q1 ≺ q2.
+#p1 #p2 * -p1 -p2
+[ #o #q #o0 #q1 #q2 #H destruct
+| #p #q #o0 #q1 #q2 #H1 #H2 destruct
+| #p #q #o0 #q1 #q2 #H1 #H2 destruct
+| #o #p #q #Hpq #o0 #q1 #q2 #H1 #H2 destruct //
+| #o0 #q1 #q2 #_ #H destruct
+]
+qed-.
+
 lemma sprec_fwd_in_whd: ∀p,q. p ≺ q → in_whd q → in_whd p.
 #p #q #H elim H -p -q // /2 width=1/
 [ #p #q * #H destruct