[STATEMENT]
lemma "w \<le>p w \<Longrightarrow> \<^bold>|w\<^bold>| = 2 \<Longrightarrow> w \<in> lists {a,b} \<Longrightarrow> hd w = a \<Longrightarrow>  w = [a, b] \<or> w = [a, a]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>w \<le>p w; \<^bold>|w\<^bold>| = 2; w \<in> lists {a, b}; hd w = a\<rbrakk> \<Longrightarrow> w = [a, b] \<or> w = [a, a]
[PROOF STEP]
by list_inspection