proposition: Lemma emptySubst_correct : forall M, correct_subst M emptySubst.
proof: Proof. split. intros i j; destruct i; try_solve. simpl; apply env_comp_sym; apply env_comp_empty. simpl; apply env_comp_sym; apply env_comp_empty. Qed.
imports: CoLoR(RelExtras ListPermutation TermsConv ListUtil ListExtras LogicUtil) Coq(Arith Lia)