(* PARALLEL SUBSTITUTION ON LOCAL ENVIRONMENTS ******************************)
lemma ltps_ldrop_conf_ge: ∀L0,L1,d1,e1. L0 [d1, e1] ≫ L1 →
(* PARALLEL SUBSTITUTION ON LOCAL ENVIRONMENTS ******************************)
lemma ltps_ldrop_conf_ge: ∀L0,L1,d1,e1. L0 [d1, e1] ≫ L1 →