proposition: Lemma envSubst_add: forall Q i j, envSub Q i j \/ (forall x, ~envSub Q i x /\ ~envSub Q x j) -> exists Q', Q' |=> Q /\ envSub Q' i j /\ (forall p q, envSub Q' p q -> (envSub Q p q \/ (p = i /\ q = j))).
proof: Proof. intros. exists (addEnvSubst Q i j H); fo. Qed.
imports: CoLoR(RelExtras ListPermutation TermsPos ListUtil ListExtras LogicUtil) Coq(Compare_dec Setoid Morphisms Lia PeanoNat)