# Re: [isabelle] How does one reason about the subset of a list?

```Hello,
I corrected the specification and simplified it so that P is valid on the entire list (to make the proof simpler for me).

P now looks like:
constdefs
"P (xs::nat list) Y == \<forall>i < length xs. xs!i \<le> Y"

And the lemma I am trying to prove is:
lemma "P xs Y \<longrightarrow> (\<forall> j. j < (length xs - 1) \<longrightarrow> P (listswap xs j (j+1)) Y)"

And I am still using the listswap and listswap_length.

I have tried to prove that lemma in different ways and failed.
The formulation of the proof which reflects my current try looks like:

lemma "P xs Y \<longrightarrow> (\<forall> j. j < (length xs - 1) \<longrightarrow> P (listswap xs j (j+1)) Y)"
have "P xs Y \<longrightarrow> (\<forall> j. Suc j < length xs \<longrightarrow>
(\<forall>i. i < length xs \<longrightarrow>
(i \<noteq> j \<and> i \<noteq> (Suc j)
\<longrightarrow> (listswap xs j (Suc j))!i \<le> Y))) "
also have "P xs Y \<longrightarrow> (\<forall> j. Suc j < length xs \<longrightarrow>
(\<forall>i. i = j \<longrightarrow> (listswap xs j (Suc j))!j \<le> Y))"
oops
also have "P xs Y \<longrightarrow> (\<forall> j. Suc j < length xs \<longrightarrow>
(\<forall>i. (i = (Suc j)) \<longrightarrow> (listswap xs j (Suc j))!(Suc j) \<le> Y))"
finally show ?thesis apply ()
qed

With the oops showing where it breaks.
Isn't this a valid way of breaking down this proof?