proposition: Lemma conv_subst_correct M M' G G' S : M ~(S) M' -> envMinimal M' -> G ~~(S) G' -> subst_envs_comp G' -> subst_envMinimal G' -> correct_subst M G -> correct_subst M' G'.
proof: Proof. intros MM' M'min GG' G'comp G'min MG. constructor; trivial. intros p A B pG' pM'. destruct (subst_dom_varSubst_rev G' pG') as [W [G'W WA]]. destruct GG'. destruct (sc_inj_r0 p W G'W) as [q qp]. destruct MG as [envsMG domMG ranMG]. apply (domMG q A B). destruct (sc_rl0 q p W qp G'W) as [W' [GW' WW']]. rewrite <- WA. assert (W_W': W' ~ W). exists S; trivial. rewrite <- (terms_conv_eq_type W_W'). apply subst_dom_varSubst; trivial. destruct MM'. apply activeEnv_subset. apply (proj2 (H0 q p qp B)). rewrite <- M'min; trivial. intros p A B pG'G' pM'. set (pG' := env_sub_suby_ly (subst_ran G') (subst_dom G') pG'G'). destruct (subst_ran_decl G' pG') as [W [i [G'i Wp]]]. destruct (sc_inj_r GG' G'i) as [m ml]. destruct (sc_rl GG' m ml G'i) as [W' [GmW' WW']]. destruct MG as [envsMG domMG ranMG]. set (Wmin := G'min i W G'i). rewrite Wmin in Wp. destruct (terms_conv_activeEnv_rev WW' Wp) as [q qp]. apply (ranMG q A B). apply env_sub_ly_rn. apply (subst_ran_decl_conv) with G' S p; trivial. apply subst_dom_varNotSubst. apply conv_subst_udecl with G' (envSubst_transp S) p. apply subst_conv_sym; destruct GG'; constructor; trivial. destruct S; trivial. apply subst_dom_varNotSubst_rev. apply env_sub_suby_rn with (subst_ran G') A; trivial. destruct MM'. apply activeEnv_subset. apply (proj2 (H0 q p qp B)). rewrite <- M'min; trivial. Qed.
imports: CoLoR(RelExtras ListExtras TermsSubst) Coq(Arith Lia)