(* Main properties **********************************************************)
-theorem csn_aaa: â\88\80L,T,A. L â\8a¢ T ÷ A â\86\92 L â\8a¢ â\87\93 T.
+theorem csn_aaa: â\88\80L,T,A. L â\8a¢ T ÷ A â\86\92 L â\8a¢ â¬\87* T.
#L #T #A #H
@(acp_aaa … csn_acp csn_acr … H)
qed.