proposition: Lemma lift_fold_1in : forall M n, lift (lift M 1) n = lift M (S n).
proof: Proof. intros. replace (S n) with (1 + n). rewrite lift_fold; trivial. lia. Qed.
imports: Coq(Compare_dec Arith Lia) CoLoR(RelExtras ListExtras LogicUtil)