(* Properties on atomic arity assignment for terms **************************)
-lemma scpds_aaa_conf: ∀h,g,G,L,d. Conf3 … (aaa G L) (scpds h g d G L).
-#h #g #G #L #d #A #T #HT #U * /3 width=6 by lstas_aaa_conf, cprs_aaa_conf/
+lemma scpds_aaa_conf: ∀h,o,G,L,d. Conf3 … (aaa G L) (scpds h o d G L).
+#h #o #G #L #d #A #T #HT #U * /3 width=6 by lstas_aaa_conf, cprs_aaa_conf/
qed.