proposition: Lemma prefix_antisymmetric: forall xs ys, prefix xs ys -> prefix ys xs -> xs = ys.
proof: Proof. Proof using. introv (ws&Ex) (zs&Ey). subst ys. rew_list in *. forwards Ey': app_l_eq_self_inv (rm Ey). forwards (E1&E2): app_eq_nil_inv (rm Ey'). subst. rew_list~. Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibOperation LibProd LibOption LibNat LibInt LibWf LibMonoid LibRelation LibList)