- basics: some support for abstract triangular confluence (which

[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 b658f9bc81cdc70114e21f63145dff10a3088510..93e22f77afe392ca40be237d6061d0b57041fe87 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
@@ -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 …).