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