proposition: Lemma prefix_cons_inverse: forall xs y ys, prefix xs (y :: ys) -> xs = nil \/ exists xs', xs = y :: xs' /\ prefix xs' ys.
proof: Proof. Proof using. introv (zs&Heq). destruct xs; [ eauto | right ]. rew_list in Heq. injects Heq. unfold prefix. eauto. Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibOperation LibProd LibOption LibNat LibInt LibWf LibMonoid LibRelation LibList)