(* Main properties concerning atomic arity assignment ***********************)
-theorem csn_aaa: ∀h,g,L,T,A. ⦃G, L⦄ ⊢ T ⁝ A → ⦃G, L⦄ ⊢ ⬊*[h, g] T.
-#h #g #L #T #A #H
+theorem aaa_csn: ∀h,g,G,L,T,A. ⦃G, L⦄ ⊢ T ⁝ A → ⦃G, L⦄ ⊢ ⬊*[h, g] T.
+#h #g #G #L #T #A #H
@(acp_aaa … (csn_acp h g) (csn_acr h g) … H)
qed.