[STATEMENT]
lemma lmirror_llist_of [simp]: "lmirror (llist_of xs) = llist_of (xs @ rev xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lmirror (llist_of xs) = llist_of (xs @ rev xs)
[PROOF STEP]
by(induct xs)(simp_all add: lappend_llist_of_LCons)