proposition: Lemma ScR_idRen {Γ Γ'} (s : Sub Γ Γ') : ScR s idRen = s.
proof: Proof. induction s; simp ScR; auto. now rewrite RenExp_idRen, IHs. Qed.
imports: Coq.Lists.List Category.Lib Category.Instance.Lambda.Exp Category.Instance.Lambda.Value Category.Instance.Lambda.Ren Equations(Equations)