proposition: Lemma lift_subst_distr : forall G H i, lift_subst (G ++ H) i = lift_subst G i ++ lift_subst H i.
proof: Proof. induction G; trivial. intros H i; simpl. rewrite (IHG H i); trivial. Qed.
imports: Coq(Compare_dec Arith Lia) CoLoR(RelExtras ListExtras LogicUtil)