[STATEMENT]
lemma iIN_cut_less1: "
  \<lbrakk> t \<in> [n\<dots>,d]; n < t \<rbrakk> \<Longrightarrow> [n\<dots>,d] \<down>< t = [n\<dots>, t - Suc n]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>t \<in> [n\<dots>,d]; n < t\<rbrakk> \<Longrightarrow> [n\<dots>,d] \<down>< t = [n\<dots>,t - Suc n]
[PROOF STEP]
by (simp add: iIN_cut_less iT_iff)