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