proposition: Lemma subst_dom_lifted_Empty G : isEmptySubst G -> emptyEnv (subst_dom (lift_subst G 1)).
proof: Proof. intro. apply subst_dom_Empty. apply subst_lift_empty; trivial. Qed.
imports: CoLoR(RelExtras ListPermutation TermsConv ListUtil ListExtras LogicUtil) Coq(Arith Lia)