- "functional" component moved to Apps_2

[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 1326a8bb482d556adf75daa324d495250180b580..01d983c0cd0435af8e263b772932f77738fdcf92 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
@@ -43,15 +43,6 @@ qed.
 
 (* Advanced properties ******************************************************)
 
-lemma csn_acp: acp cpr (eq …) (csn …).
-@mk_acp
-[ /2 width=1/
-| /2 width=3/
-| /2 width=5/
-| @cnf_lift
-]
-qed.
-
 (* Basic_1: was: sn3_abbr *)
 lemma csn_lref_abbr: ∀L,K,V,i. ⇩[0, i] L ≡ K. ⓓV → K ⊢ ⬇* V → L ⊢ ⬇* #i.
 #L #K #V #i #HLK #HV
@@ -96,3 +87,14 @@ elim (eq_false_inv_tpair_dx … H2) -H2
   @IHT1 -IHT1 // -HLT02 /2 width=1/
 ]
 qed.
+
+(* Main properties **********************************************************)
+
+theorem csn_acp: acp cpr (eq …) (csn …).
+@mk_acp
+[ /2 width=1/
+| /2 width=3/
+| /2 width=5/
+| @cnf_lift
+]
+qed.