(* Note: it does not hold replacing |L1| with |L2| *)
(* Basic_1: was only: pr2_change *)
lemma cpr_lsubs_conf: ∀L1,T1,T2. L1 ⊢ T1 ➡ T2 →
(* Note: it does not hold replacing |L1| with |L2| *)
(* Basic_1: was only: pr2_change *)
lemma cpr_lsubs_conf: ∀L1,T1,T2. L1 ⊢ T1 ➡ T2 →