proposition: Lemma conv_env_lift : forall M n, conv_env M (lift M n) (liftEnvSubst n 0 (length (env M))).
proof: Proof. intros. intros x y Qxy A. rewrite (activeEnv_lift M n). unfold liftedEnv; autorewrite with datatypes terms using simpl. inversion Qxy; unfold VarD. destruct (le_gt_dec 0 x); try solve [lia]. split; intro D. rewrite <- H0. rewrite nth_app_right; autorewrite with datatypes using try lia. replace (x + n - n) with x; [trivial | lia]. rewrite <- H0 in D. rewrite nth_app_right in D; autorewrite with datatypes using try lia. replace (x + n - length (copy n (None (A:=SimpleType)))) with x in D; trivial. autorewrite with datatypes using lia. Qed.
imports: CoLoR(RelExtras ListPermutation TermsPos ListUtil ListExtras LogicUtil) Coq(Compare_dec Setoid Morphisms Lia PeanoNat)