[STATEMENT]
lemma lrev_is_LNil_conv [iff]:
  "xs \<in> UNIV\<^sup>\<star> \<Longrightarrow> (lrev xs = LNil) = (xs = LNil)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xs \<in> UNIV\<^sup>\<star> \<Longrightarrow> (lrev xs = LNil) = (xs = LNil)
[PROOF STEP]
by (induct rule: finlsts.induct) auto