proposition: Lemma idSubst_correct M : correct_subst M (idSubst M).
proof: Proof. destruct M as [envM ???]. unfold idSubst; simpl. destruct (isVarDecl_dec envM 0) as [[A EA] | En]. simpl; apply one_var_subst_correct; simpl. intros; inversion EA; inversion H; try_solve. apply env_comp_refl. simpl; apply one_var_subst_correct; simpl. intros A E0; inversion E0; inversion En; destruct envM; try_solve. destruct envM. apply env_comp_sym; apply env_comp_empty. destruct o. inversion En; try_solve. unfold decl; apply env_comp_cons; auto. apply env_comp_empty. Qed.
imports: CoLoR(RelExtras ListPermutation TermsConv ListUtil ListExtras LogicUtil) Coq(Arith Lia)