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