proposition: Lemma envSubst_lift1_ext : forall Q Q', Q' |=> Q -> envSubst_lift1 Q' |=> envSubst_lift1 Q.
proof: Proof. intros Q Q' Q'Q p q Qpq. destruct p; destruct q; destruct Q; destruct Q'; fo. Qed.
imports: CoLoR(RelExtras ListPermutation TermsPos ListUtil ListExtras LogicUtil) Coq(Compare_dec Setoid Morphisms Lia PeanoNat)