(* *)
(**************************************************************************)
-include "Basic_2/computation/acp_aaa.ma".
-include "Basic_2/computation/csn_lcpr_vector.ma".
+include "basic_2/computation/acp_aaa.ma".
+include "basic_2/computation/csn_tstc_vector.ma".
(* CONTEXT-SENSITIVE STRONGLY NORMALIZING TERMS *****************************)
(* Properties concerning atomic arity assignment ****************************)
-lemma 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.