X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambda_delta%2Fbasic_2%2Fcomputation%2Fcsn_lift.ma;h=93e22f77afe392ca40be237d6061d0b57041fe87;hb=390de3f72df749a6f153e59e2620503657ce9eab;hp=b658f9bc81cdc70114e21f63145dff10a3088510;hpb=a8c166f1e1baeeae04553058bd179420ada8bbe7;p=helm.git

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 b658f9bc8..93e22f77a 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/computation/csn_lift.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/computation/csn_lift.ma
@@ -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 …).