proposition: Lemma prefix_cons_cons_inverse: forall x1 x2 xs1 xs2, prefix (x1 :: xs1) (x2 :: xs2) -> x1 = x2 /\ prefix xs1 xs2.
proof: Proof. Proof using. intros. forwards: prefix_cons_inverse; eauto. branches; unpack; try split; congruence. Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibOperation LibProd LibOption LibNat LibInt LibWf LibMonoid LibRelation LibList)