proposition: Lemma equiv_app: forall L1 L2 L3 L4, Equiv L1 L3 -> Equiv L2 L4 -> Equiv (App L1 L2) (App L3 L4).
proof: Proof. split; intros. - eapply app_in_equiv; eauto. - eapply app_in_equiv; eauto. + apply equiv_sym. assumption. + apply equiv_sym. assumption. Qed.
imports: Coq.Lists.List