proposition: Lemma ScS_idSub_left {Γ Γ'} (σ : Sub Γ Γ') : ScS idSub σ = σ.
proof: Proof. induction σ; simpl; auto. simp SubVar. rewrite ScS_ScR. unfold skip1. simp RcS. rewrite RcS_idRen. now rewrite IHσ. Qed.
imports: Coq.Lists.List Category.Lib Category.Instance.Lambda.Exp Category.Instance.Lambda.Value Category.Instance.Lambda.Ren Equations(Equations)