(* Note: we could invoke tpss_weak_all instead of ltpr_fwd_length *)
(* Basic_1: was only: pr2_subst1 *)
lemma cpr_tpss_ltpr: ∀L1,L2. L1 ➡ L2 → ∀T1,T2. L2 ⊢ T1 ➡ T2 →
(* Note: we could invoke tpss_weak_all instead of ltpr_fwd_length *)
(* Basic_1: was only: pr2_subst1 *)
lemma cpr_tpss_ltpr: ∀L1,L2. L1 ➡ L2 → ∀T1,T2. L2 ⊢ T1 ➡ T2 →