proposition: Lemma app_assoc_in_1: forall L1 L2 L3 w, In w (App L1 (App L2 L3)) -> In w (App (App L1 L2) L3).
proof: Proof. intros. apply app_in_inv in H. destruct H as (w1, (w2, (?, (Ha, Hb)))). subst. apply app_in_inv in Hb. destruct Hb as (w3, (w4, (?, (Hc, Hd)))). subst. rewrite app_assoc. auto using app_in_eq. Qed.
imports: Coq.Lists.List