[STATEMENT]
lemma finlsts_rec_LNil_def:
  "f \<equiv> finlsts_rec c d \<Longrightarrow> f LNil = c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f \<equiv> finlsts_rec c d \<Longrightarrow> f LNil = c
[PROOF STEP]
by (auto simp: finlsts_rec_LNil)