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