proposition: Lemma singleton_correct_single M P G : correct_subst M G -> isSingletonSubst P G -> correct_subst M {x/P}.
proof: Proof. intros. destruct H. constructor. apply subst_envs_comp_single. simpl; intros p A B pA. destruct p. intro M0. replace A with (type P); trivial. apply (dom_c0 0 (type P) B); trivial. destruct (subst_dom_singleton H0) as [E [GE _]]. rewrite GE; constructor. inversion pA; trivial. inversion pA; destruct p; try_solve. simpl. rewrite (subst_ran_singleton H0) in ran_c0. rewrite subst_ran_single. destruct (subst_dom_singleton H0) as [E [GE Eempty]]. rewrite GE in ran_c0. intros p A B Pp. destruct p. exfalso. apply (varD_UD_absurd Pp). apply env_sub_ry with (type P); constructor. intros Mp. apply (ran_c0 (S p)); trivial. apply env_sub_ly_rn. apply env_sub_suby_ly with {x/type P}; trivial. unfold VarUD; simpl. apply Eempty. Qed.
imports: CoLoR(RelExtras ListPermutation TermsConv ListUtil ListExtras LogicUtil) Coq(Arith Lia)