(* Basic_1: was just: pr3_pr3_pr3_t *)
(* Note: alternative proof /3 width=5 by s_r_trans_LTC1, lprs_cpr_trans/ *)
lemma lprs_cprs_trans: ∀G. s_rs_transitive … (cpr G) (λ_. lprs G).
(* Basic_1: was just: pr3_pr3_pr3_t *)
(* Note: alternative proof /3 width=5 by s_r_trans_LTC1, lprs_cpr_trans/ *)
lemma lprs_cprs_trans: ∀G. s_rs_transitive … (cpr G) (λ_. lprs G).