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