(**************************************************************************)
include "Basic_2/computation/acp_aaa.ma".
-include "Basic_2/computation/csn_cr.ma".
+include "Basic_2/computation/csn_lcpr_vector.ma".
(* CONTEXT-SENSITIVE STRONGLY NORMALIZING TERMS *****************************)
-(* Main properties **********************************************************)
+(* Properties concerning atomic arity assignment ****************************)
-theorem csn_aaa: ∀L,T,A. L ⊢ T ÷ A → L ⊢ ⇓ T.
+lemma csn_aaa: ∀L,T,A. L ⊢ T ÷ A → L ⊢ ⬇* T.
#L #T #A #H
@(acp_aaa … csn_acp csn_acr … H)
qed.