[STATEMENT]
lemma ltl_ltakeWhile:
  "ltl (ltakeWhile P xs) = (if P (lhd xs) then ltakeWhile P (ltl xs) else LNil)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ltl (ltakeWhile P xs) = (if P (lhd xs) then ltakeWhile P (ltl xs) else LNil)
[PROOF STEP]
by(cases xs) simp_all