proposition: Lemma one_var_subst_correct M N : (forall A, env M |= 0 := A -> A = type N) -> env M [<->] env N -> correct_subst M {x/N}.
proof: Proof. intros M_x MN_comp; split. apply subst_envs_comp_single. simpl; intro p; destruct p; intros A B. intros Nx Mx. unfold VarD in Nx. inversion Nx. sym; apply M_x; trivial. unfold VarD; destruct p; simpl; intros; discr. rewrite subst_ran_single. apply env_comp_sub. apply env_comp_sym; trivial. Qed.
imports: CoLoR(RelExtras ListPermutation TermsConv ListUtil ListExtras LogicUtil) Coq(Arith Lia)