proposition: Lemma SubVar_RcS {Γ Γ' Γ'' τ} (σ : Ren Γ' Γ'') (δ : Sub Γ Γ') (v : Var Γ'' τ) : SubVar (RcS σ δ) v = SubVar δ (RenVar σ v).
proof: Proof. induction σ; simp RenVar; auto. - dependent elimination δ. now simp RcS. - dependent elimination δ. simp RcS. dependent elimination v. + now simp RenVar. + simp RenVar. now simp SubVar. Qed.
imports: Coq.Lists.List Category.Lib Category.Instance.Lambda.Exp Category.Instance.Lambda.Value Category.Instance.Lambda.Ren Equations(Equations)