proposition: Lemma subst_env M G (C: correct_subst M G) : env (subst C) = env M [-] subst_dom G [+] subst_ran G.
proof: Proof. unfold subst; intros. destruct (subst_aux C); simpl; tauto. Qed.
imports: CoLoR(RelExtras ListPermutation TermsConv ListUtil ListExtras LogicUtil) Coq(Arith Lia)