proposition: Lemma lift_subst_0 : forall (G: Subst), lift_subst G 0 = G.
proof: Proof. induction G; trivial. simpl; unfold lift_subst_comp. destruct a; try rewrite lift_0; rewrite IHG; trivial. Qed.
imports: Coq(Compare_dec Arith Lia) CoLoR(RelExtras ListExtras LogicUtil)