proposition: Lemma lift_empty_subst : forall m i, lift_subst (copy m None) i = copy m None.
proof: Proof. induction m; intro i. trivial. simpl. rewrite (IHm i); trivial. Qed.
imports: Coq(Compare_dec Arith Lia) CoLoR(RelExtras ListExtras LogicUtil)