proposition: Lemma RcS_idSub {Γ Γ'} (σ : Ren Γ Γ') : RcS σ idSub = ScR idSub σ.
proof: Proof. induction σ; simp RcS; simpl; simp RcS; simp ScR; auto. - rewrite <- ScR_RcS. rewrite IHσ. rewrite ScR_ScR. unfold skip1. simp RcR. now rewrite RcR_idRen_right. - simpl. f_equal. rewrite <- ScR_RcS. rewrite IHσ. rewrite ScR_ScR. unfold skip1. rewrite ScR_ScR. simp RcR. rewrite RcR_idRen_left. now rewrite RcR_idRen_right. Qed.
imports: Coq.Lists.List Category.Lib Category.Instance.Lambda.Exp Category.Instance.Lambda.Value Category.Instance.Lambda.Ren Equations(Equations)