proposition: Lemma envSubst_lift_lower : forall Q, envSub Q 0 0 -> envSubst_lift1 (envSubst_lower Q) <=> Q.
proof: Proof. intros; constructor; intros x y; destruct Q; destruct x; destruct y; try_solve. intro h. assert (0 = S y). eapply envSub_Lok0. apply H. hyp. discr. intro h. assert (S x = 0). eapply envSub_Rok0. apply h. hyp. discr. Qed.
imports: CoLoR(RelExtras ListPermutation TermsPos ListUtil ListExtras LogicUtil) Coq(Compare_dec Setoid Morphisms Lia PeanoNat)