proposition: Lemma SemVar_RenSem Γ τ (v : Var Γ τ) Γ' (r : Ren Γ' Γ) (se : SemEnv Γ') : SemVar v (RenSem r se) = SemVar (RenVar r v) se.
proof: Proof. intros. induction r; simp RenSem; simp RenVar; simpl; destruct se; simp RenSem; auto. 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)