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