proposition: Lemma RenSem_skip1 {Γ τ} (e : SemTy τ) (se : SemEnv Γ) : RenSem skip1 (e, se) = se.
proof: Proof. induction Γ; destruct se; simpl; intros; auto. unfold skip1; simp RenSem. now rewrite RenSem_idRen. 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)