proposition: Lemma idSubst_neutral M : (subst (idSubst_correct M)) ~ M.
proof: Proof. apply terms_conv_criterion. rewrite subst_env. destruct M as [envM ???]; unfold idSubst; simpl. destruct (isVarDecl_dec envM 0) as [[A EA] | En]; simpl. destruct envM; try destruct o; try_solve. rewrite env_sub_empty. rewrite env_sum_double. apply env_comp_refl. unfold subst_ran; simpl. destruct envM; try_solve. destruct o. inversion En; try_solve. simpl; rewrite env_sub_empty; rewrite env_sum_empty_r. apply env_comp_cons; auto. apply env_comp_refl. rewrite subst_term. unfold presubst. change (idSubst M) with (copy 0 None ++ idSubst M). apply idSubst_neutral_aux. Qed.
imports: CoLoR(RelExtras ListPermutation TermsConv ListUtil ListExtras LogicUtil) Coq(Arith Lia)