proposition: Lemma lift_subst_app : forall G1 G2 i, lift_subst (G1 ++ G2) i = lift_subst G1 i ++ lift_subst G2 i.
proof: Proof. induction G1; trivial. intros; simpl. rewrite IHG1; trivial. Qed.
imports: CoLoR(RelExtras ListPermutation TermsConv ListUtil ListExtras LogicUtil) Coq(Arith Lia)