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