[STATEMENT]
lemma tconcat_TCons [simp]: "tconcat b (TCons a tr) = lappendt a (tconcat b tr)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. tconcat b (TCons a tr) = lappendt a (tconcat b tr)
[PROOF STEP]
by transfer auto