#L #V #T1 #T2 * /3 width=3/
qed.
(* 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 →
#L #V #T1 #T2 * /3 width=3/
qed.
(* 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 →