X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=inline;f=matita%2Fmatita%2Fcontribs%2Flambda_delta%2Fbasic_2%2Freducibility%2Fltpr.ma;fp=matita%2Fmatita%2Fcontribs%2Flambda_delta%2Fbasic_2%2Freducibility%2Fltpr.ma;h=a910ea7df3f835c0520b6d1b5a6420915bf2f8f1;hb=7bedf1797ba168f0742194b2add69575e5d4a5cd;hp=67986d336f87b2a39bb3bc63a5f2a9f6a8785d75;hpb=3ca25660341410dd0f8694e6863c7c16f4e912a7;p=helm.git

diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/ltpr.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/ltpr.ma
index 67986d336..a910ea7df 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/ltpr.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/ltpr.ma
@@ -28,6 +28,9 @@ interpretation
 lemma ltpr_refl: reflexive … ltpr.
 /2 width=1/ qed.
 
+lemma ltpr_append: ∀K1,K2. K1 ➡ K2 → ∀L1,L2:lenv. L1 ➡ L2 → K1 @@ L1 ➡ K2 @@ L2.
+/2 width=1/ qed.
+
 (* Basic inversion lemmas ***************************************************)
 
 (* Basic_1: was: wcpr0_gen_sort *)
@@ -51,4 +54,14 @@ lemma ltpr_inv_pair2: ∀L1,K2,I,V2. L1 ➡ K2. ⓑ{I} V2 →
 lemma ltpr_fwd_length: ∀L1,L2. L1 ➡ L2 → |L1| = |L2|.
 /2 width=2 by lpx_fwd_length/ qed-.
 
+(* Advanced inversion lemmas ************************************************)
+
+lemma ltpr_inv_append1: ∀K1,L1. ∀L:lenv. K1 @@ L1 ➡ L →
+                        ∃∃K2,L2. K1 ➡ K2 & L1 ➡ L2 & L = K2 @@ L2.
+/2 width=1 by lpx_inv_append1/ qed-.
+
+lemma ltpr_inv_append2: ∀L:lenv. ∀K2,L2. L ➡ K2 @@ L2 →
+                        ∃∃K1,L1. K1 ➡ K2 & L1 ➡ L2 & L = K1 @@ L1.
+/2 width=1 by lpx_inv_append2/ qed-.
+
 (* Basic_1: removed theorems 2: wcpr0_getl wcpr0_getl_back *)