proposition: Lemma app_in_equiv: forall L1 L2 L3 L4 w, Equiv L1 L3 -> Equiv L2 L4 -> In w (App L1 L2) -> In w (App L3 L4).
proof: Proof. intros. apply app_in_inv in H1. destruct H1 as (w1, (w2, (?, (Ha, Hb)))). subst. apply app_in_eq. + apply H; assumption. + apply H0. assumption. Qed.
imports: Coq.Lists.List