proposition: Lemma RcS_skip1 {Γ Γ' τ} (e : Exp Γ τ) (σ : Sub Γ Γ') : RcS skip1 (Push e σ) = σ.
proof: Proof. unfold skip1. simp RcS. now rewrite RcS_idRen. Qed.
imports: Coq.Lists.List Category.Lib Category.Instance.Lambda.Exp Category.Instance.Lambda.Value Category.Instance.Lambda.Ren Equations(Equations)