- property S6 of stronfly normalizing terms proved

[helm.git] / matita / matita / contribs / lambda_delta / Basic_2 / computation / cprs.ma

diff --git a/matita/matita/contribs/lambda_delta/Basic_2/computation/cprs.ma b/matita/matita/contribs/lambda_delta/Basic_2/computation/cprs.ma
index 3e4289e2789c15746290db3fb9f542ced9aef8ea..12cd0791f0420257af63ad6f10512818c237332e 100644 (file)
--- a/matita/matita/contribs/lambda_delta/Basic_2/computation/cprs.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/computation/cprs.ma
@@ -63,4 +63,23 @@ lemma cprs_flat_dx: ∀I,L,V1,V2. L ⊢ V1 ➡ V2 → ∀T1,T2. L ⊢ T1 ➡* T2
 @(cprs_strap1 … IHT2) -IHT2 /2 width=1/
 qed.
 
+(* Basic inversion lemmas ***************************************************)
+
+(* Basic_1: was: pr3_gen_sort *)
+lemma cprs_inv_sort1: ∀L,U2,k. L ⊢ ⋆k ➡* U2 → U2 = ⋆k.
+#L #U2 #k #H @(cprs_ind … H) -U2 //
+#U2 #U #_ #HU2 #IHU2 destruct
+>(cpr_inv_sort1 … HU2) -HU2 //
+qed-.
+
+(* Basic_1: was: pr3_gen_cast *)
+lemma cprs_inv_cast1: ∀L,W1,T1,U2. L ⊢ ⓣW1.T1 ➡* U2 → L ⊢ T1 ➡* U2 ∨
+                      ∃∃W2,T2. L ⊢ W1 ➡* W2 & L ⊢ T1 ➡* T2 & U2 = ⓣW2.T2.
+#L #W1 #T1 #U2 #H @(cprs_ind … H) -U2 /3 width=5/
+#U2 #U #_ #HU2 * /3 width=3/ *
+#W #T #HW1 #HT1 #H destruct
+elim (cpr_inv_cast1 … HU2) -HU2 /3 width=3/ *
+#W2 #T2 #HW2 #HT2 #H destruct /4 width=5/
+qed-.
+
 (* Basic_1: removed theorems 2: clear_pr3_trans pr3_cflat *)