proposition: Lemma subst_ran_decl_conv G G' S x y A : G ~~(S) G' -> envSub S x y -> subst_envs_comp G -> subst_envMinimal G' -> subst_ran G' |= y := A -> subst_ran G |= x := A.
proof: Proof. intros GG' Sxy G'comp G'min G'x. destruct (subst_ran_decl G' G'x) as [W [p [Gp Wx]]]. destruct (sc_inj_r GG' Gp) as [q pq]. destruct (sc_rl GG' q pq Gp) as [W' [G'W' WW']]. apply subst_ran_component_comp with q W'; trivial. apply activeEnv_subset. apply (proj2 (proj2 WW' x y Sxy A)); trivial. rewrite <- G'min with p W; trivial. Qed.
imports: CoLoR(RelExtras ListExtras TermsSubst) Coq(Arith Lia)