proposition: Lemma sumEnvSubst_ext_l : forall Q Ql Qr (QQl: Q |=> Ql) (QQr: Q |=> Qr), sumEnvSubst QQl QQr |=> Ql.
proof: Proof. intros; intros p q pq; simpl; auto. Qed.
imports: CoLoR(RelExtras ListPermutation TermsPos ListUtil ListExtras LogicUtil) Coq(Compare_dec Setoid Morphisms Lia PeanoNat)