proposition: Lemma subst_dom_lifted : forall G n, subst_dom (lift_subst G n) = subst_dom G.
proof: Proof. induction G. auto. intros n; simpl; unfold lift_subst_comp. rewrite IHG. destruct a; trivial. rewrite lift_type; trivial. Qed.
imports: CoLoR(RelExtras ListPermutation TermsConv ListUtil ListExtras LogicUtil) Coq(Arith Lia)