proposition: Lemma lift_subst_fold : forall G m n, lift_subst G (m+n) = lift_subst (lift_subst G m) n.
proof: Proof. induction G. trivial. intros m n; simpl. rewrite (IHG m n). destruct a; simpl. rewrite lift_fold; trivial. trivial. Qed.
imports: Coq(Compare_dec Arith Lia) CoLoR(RelExtras ListExtras LogicUtil)