/2 width=3/ qed.
(* Note: it does not hold replacing |L1| with |L2| *)
-lemma cprs_lsubs_conf: ∀L1,T1,T2. L1 ⊢ T1 ➡* T2 →
- ∀L2. L1 ≼ [0, |L1|] L2 → L2 ⊢ T1 ➡* T2.
+lemma cprs_lsubs_trans: ∀L1,T1,T2. L1 ⊢ T1 ➡* T2 →
+ ∀L2. L2 ≼ [0, |L1|] L1 → L2 ⊢ T1 ➡* T2.
/3 width=3/
qed.