matita/matita/contribs/lambdadelta/basic_2/etc/lprs/lprs.etc

   1 lemma lprs_cpr_trans: ∀G. b_c_transitive … (cpr G) (λ_. lprs G).
   2 /3 width=5 by b_c_trans_CTC2, lpr_cprs_trans/ qed-.
   3
   4 (* Basic_1: was just: pr3_pr3_pr3_t *)
   5 (* Note: alternative proof /3 width=5 by s_r_trans_CTC1, lprs_cpr_trans/ *)
   6 lemma lprs_cprs_trans: ∀G. b_rs_transitive … (cpr G) (λ_. lprs G).
   7 #G @b_c_to_b_rs_trans @b_c_trans_CTC2
   8 @b_rs_trans_TC1 /2 width=3 by lpr_cprs_trans/ (**) (* full auto too slow *)
   9 qed-.