X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fmatita%2Fcontribs%2Flambda_delta%2FBasic_2%2Fcomputation%2Fcsn_lift.ma;h=01d983c0cd0435af8e263b772932f77738fdcf92;hb=10fa9ea840893d1b452200a402612f923765967e;hp=1326a8bb482d556adf75daa324d495250180b580;hpb=3443885ee60fbcb90e2d106e67d3b7f7e3c59bad;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 1326a8bb4..01d983c0c 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
@@ -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.