proposition: Lemma ScR_RcS {Γ Γ' Γ'' Γ'''} (σ : Ren Γ'' Γ''') (δ : Sub Γ' Γ'') (ν : Ren Γ Γ') : ScR (RcS σ δ) ν = RcS σ (ScR δ ν).
proof: Proof. induction σ; dependent elimination δ; auto. - simp RcS. now simp ScR. - simp RcS. simp ScR. simp RcS. now rewrite IHσ. Qed.
imports: Coq.Lists.List Category.Lib Category.Instance.Lambda.Exp Category.Instance.Lambda.Value Category.Instance.Lambda.Ren Equations(Equations)