proposition: Lemma app_l_char_in_inv: forall c L w, In w (App (Char c) L) -> exists w', w = c:: w' /\ In w' L.
proof: Proof. intros. apply app_in_inv in H. destruct H as (w1, (w2, (?, (Ha, Hb)))). apply char_in_inv in Ha. subst. exists w2. auto. Qed.
imports: Coq.Lists.List