proposition: Lemma SemExp_wk `(E : SemEnv Γ) {τ τ'} (y : SemTy τ') (e : Exp Γ τ) : SemExp (wk e) (y, E) = SemExp e E.
proof: Proof. unfold wk. rewrite <- SemExp_RenSem; simpl. f_equal. now rewrite RenSem_skip1. 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)