proposition: Lemma envSubst_lift1_absurdL : forall i Q, envSub (envSubst_lift1 Q) (S i) 0 -> False.
proof: Proof. intros i Q p. absurd (S i = 0); try_solve. apply envSub_Rok with (envSubst_lift1 Q) 0; trivial. destruct Q; simpl; trivial. Qed.
imports: CoLoR(RelExtras ListPermutation TermsPos ListUtil ListExtras LogicUtil) Coq(Compare_dec Setoid Morphisms Lia PeanoNat)