/4 width=5 by cpm_fwd_cpx, rpx_fsge_comp, rex_co/ qed-.
(* Properties with generic extension on referred entries ********************)
(* Basic_2A1: was just: cpr_llpx_sn_conf *)
/4 width=5 by cpm_fwd_cpx, rpx_fsge_comp, rex_co/ qed-.
(* Properties with generic extension on referred entries ********************)
(* Basic_2A1: was just: cpr_llpx_sn_conf *)