proposition: Lemma ScR_ScS {Γ Γ' Γ'' Γ'''} (σ : Sub Γ'' Γ''') (δ : Sub Γ' Γ'') (ν : Ren Γ Γ') : ScR (ScS σ δ) ν = ScS σ (ScR δ ν).
proof: Proof. generalize dependent Γ'. generalize dependent Γ. induction σ; simp ScR; simp ScS; simpl; intros; auto. simp ScR. rewrite IHσ. f_equal. now rewrite <- SubExp_ScR. Qed.
imports: Coq.Lists.List Category.Lib Category.Instance.Lambda.Exp Category.Instance.Lambda.Value Category.Instance.Lambda.Ren Equations(Equations)