(* *)
(**************************************************************************)
-include "basic_2/unfold/lsstas_aaa.ma".
+include "basic_2/unfold/lstas_aaa.ma".
include "basic_2/computation/cpxs_aaa.ma".
include "basic_2/computation/cpds.ma".
(* Properties on atomic arity assignment for terms **************************)
-lemma aaa_cpds_conf: ∀h,g,G,L. Conf3 … (aaa G L) (cpds h g G L).
-#h #g #G #L #A #T #HT #U * /3 width=6 by aaa_lsstas_conf, aaa_cprs_conf/
+lemma cpds_aaa_conf: ∀h,g,G,L. Conf3 … (aaa G L) (cpds h g G L).
+#h #g #G #L #A #T #HT #U * /3 width=6 by lstas_aaa_conf, cprs_aaa_conf/
qed.