proposition: Lemma RcS_DropAll {Γ Γ'} (σ : Sub Γ' Γ) : RcS DropAll σ = NoSub.
proof: Proof. now induction σ; simp RcS. Qed.
imports: Coq.Lists.List Category.Lib Category.Instance.Lambda.Exp Category.Instance.Lambda.Value Category.Instance.Lambda.Ren Equations(Equations)