(* ABSTRACT COMPUTATION PROPERTIES ******************************************)
-(* Main propertis ***********************************************************)
+(* Main properties **********************************************************)
(* Basic_1: was: sc3_arity_csubc *)
theorem aacr_aaa_csubc_lifts: ∀RR,RS,RP.