proposition: Lemma lift_type : forall M n, type (lift M n) = type M.
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)