proposition: Lemma SemVar_SubSem {Γ Γ' τ} (v : Var Γ τ) (s : Sub Γ' Γ) (se : SemEnv Γ') : SemVar v (SubSem s se) = SemExp (SubVar s v) se.
proof: Proof. intros. induction s; simp SubSem; simp SubVar; simpl. - now inversion v. - now dependent elimination v; simpl; simp RenVar. Qed.
imports: Category.Lib Category.Lib.IList Category.Instance.Lambda.Ty Category.Instance.Lambda.Exp Category.Instance.Lambda.Ren Category.Instance.Lambda.Sub Equations(Equations)