- relation between native type and atomic arity proced

[helm.git] / matita / matita / contribs / lambda_delta / basic_2 / computation / csn_lift.ma

diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/csn_lift.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/csn_lift.ma
index 01d983c0cd0435af8e263b772932f77738fdcf92..85cdef226346824371ae67c4723e16c85a1d9b54 100644 (file)
--- a/matita/matita/contribs/lambda_delta/basic_2/computation/csn_lift.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/computation/csn_lift.ma
@@ -12,9 +12,9 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "Basic_2/reducibility/cnf_lift.ma".
-include "Basic_2/computation/acp.ma".
-include "Basic_2/computation/csn.ma".
+include "basic_2/reducibility/cnf_lift.ma".
+include "basic_2/computation/acp.ma".
+include "basic_2/computation/csn.ma".
 
 (* CONTEXT-SENSITIVE STRONGLY NORMALIZING TERMS *****************************)
 
@@ -27,7 +27,7 @@ lemma csn_lift: ∀L2,L1,T1,d,e. L1 ⊢ ⬇* T1 →
 @csn_intro #T #HLT2 #HT2
 elim (cpr_inv_lift … HL21 … HT12 … HLT2) -HLT2 #T0 #HT0 #HLT10
 @(IHT1 … HLT10) // -L1 -L2 #H destruct
->(lift_mono … HT0 … HT12) in HT2; -T0 /2 width=1/
+>(lift_mono … HT0 … HT12) in HT2; -T1 /2 width=1/
 qed.
 
 (* Basic_1: was: sn3_gen_lift *)
@@ -38,7 +38,7 @@ lemma csn_inv_lift: ∀L2,L1,T1,d,e. L1 ⊢ ⬇* T1 →
 elim (lift_total T d e) #T0 #HT0
 lapply (cpr_lift … HL12 … HT21 … HT0 HLT2) -HLT2 #HLT10
 @(IHT1 … HLT10) // -L1 -L2 #H destruct
->(lift_inj … HT0 … HT21) in HT2; -T0 /2 width=1/
+>(lift_inj … HT0 … HT21) in HT2; -T1 /2 width=1/
 qed.
 
 (* Advanced properties ******************************************************)
@@ -70,8 +70,8 @@ elim (eq_false_inv_tpair_sn … H2) -H2
 qed.
 
 lemma csn_appl_simple: ∀L,V. L ⊢ ⬇* V → ∀T1.
-                       (∀T2. L ⊢ T1 ➡ T2 → (T1 = T2 → False) → L ⊢ ⬇* ⓐV. T2) →
-                       𝐒[T1] → L ⊢ ⬇* ⓐV. T1.
+                       (∀T2. L ⊢ T1 ➡ T2 → (T1 = T2 → ⊥) → L ⊢ ⬇* ⓐV. T2) →
+                       𝐒⦃T1⦄ → L ⊢ ⬇* ⓐV. T1.
 #L #V #H @(csn_ind … H) -V #V #_ #IHV #T1 #IHT1 #HT1
 @csn_intro #X #H1 #H2
 elim (cpr_inv_appl1_simple … H1 ?) // -H1
@@ -88,6 +88,17 @@ elim (eq_false_inv_tpair_dx … H2) -H2
 ]
 qed.
 
+(* Advanced inversion lemmas ************************************************)
+
+(* Basic_1: was: sn3_gen_def *)
+lemma csn_inv_lref_abbr: ∀L,K,V,i. ⇩[0, i] L ≡ K. ⓓV → L ⊢ ⬇* #i → K ⊢ ⬇* V.
+#L #K #V #i #HLK #Hi
+elim (lift_total V 0 (i+1)) #V0 #HV0
+lapply (ldrop_fwd_ldrop2 … HLK) #H0LK
+@(csn_inv_lift … H0LK … HV0) -H0LK
+@(csn_cpr_trans … Hi) -Hi /2 width=6/
+qed-.
+
 (* Main properties **********************************************************)
 
 theorem csn_acp: acp cpr (eq …) (csn …).