proposition: Lemma SubVar_ScS {Γ Γ' Γ'' τ} (σ : Sub Γ' Γ'') (δ : Sub Γ Γ') (v : Var Γ'' τ) : SubVar (ScS σ δ) v = SubExp δ (SubVar σ v).
proof: Proof. induction σ; simp SubVar; simp ScR. - now inversion v. - simpl. now dependent elimination v; simp SubVar. Qed.
imports: Coq.Lists.List Category.Lib Category.Instance.Lambda.Exp Category.Instance.Lambda.Value Category.Instance.Lambda.Ren Equations(Equations)