proposition: Lemma lift_env : forall M n, env (lift M n) = liftedEnv n (env M) 0.
proof: Proof. intros; unfold lift. destruct (lift_aux n M 0) as [M' [env_M' [term_M' type_M']]]. trivial. Qed.
imports: Coq(Compare_dec Arith Lia) CoLoR(RelExtras ListExtras LogicUtil)